Skip to content

[Merged by Bors] - feat(InfinitePlace/Ramification): embeddings of unramified/ramified infinite places satisfy IsUnmixed/IsMixed#29946

Closed
smmercuri wants to merge 11 commits intoleanprover-community:masterfrom
smmercuri:IsRamified-IsMixed
Closed

[Merged by Bors] - feat(InfinitePlace/Ramification): embeddings of unramified/ramified infinite places satisfy IsUnmixed/IsMixed#29946
smmercuri wants to merge 11 commits intoleanprover-community:masterfrom
smmercuri:IsRamified-IsMixed

Conversation

@smmercuri
Copy link
Copy Markdown
Collaborator

@smmercuri smmercuri commented Sep 24, 2025 •
edited
Loading

@smmercuri smmercuri mentioned this pull request Sep 24, 2025
Open
7 tasks
@github-actions github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Sep 24, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 24, 2025 •
edited
Loading

PR summary 66b2a6571b

Import changes for modified files

No significant changes to the import graph
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py
M scripts/count-trans-deps.py

Import changes for all files
Files Import difference

Declarations diff

+ IsRamified.comap_embedding
+ IsRamified.comap_embedding_conjugate
+ IsRamified.isComplex
+ IsRamified.isMixed_conjugate_embedding
+ IsRamified.isMixed_embedding
+ IsRamified.isReal
+ IsUnramified.isUnmixed
+ IsUnramified.isUnmixed_conjugate
+ comap_embedding_of_isReal
+ isRamified_mk_iff_isMixed
+ isUnramified_mk_iff_isUnmixed

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 24, 2025
@smmercuri smmercuri added FLT part of the ongoing formalization of Fermat's Last Theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Sep 24, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 28, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Sep 28, 2025

This PR/issue depends on:

@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 28, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Sep 28, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 29, 2025
xroblot
xroblot approved these changes Oct 9, 2025
View reviewed changes
Copy link
Copy Markdown
Collaborator

@xroblot xroblot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, but I have the feeling some iff results should/could be added

@smmercuri
Copy link
Copy Markdown
Collaborator Author

smmercuri commented Oct 9, 2025

LGTM, but I have the feeling some iff results should/could be added

Agree, added those in!

@smmercuri smmercuri mentioned this pull request Oct 15, 2025
Open
9 tasks
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 29, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Oct 29, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 29, 2025
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
@mathlib4-merge-conflict-bot
Copy link
Copy Markdown
Collaborator

mathlib4-merge-conflict-bot commented Nov 19, 2025

This pull request has conflicts, please merge master and resolve them.

@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025
riccardobrasca
riccardobrasca approved these changes Nov 24, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 24, 2025

✌️ smmercuri can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Nov 24, 2025
@smmercuri
Copy link
Copy Markdown
Collaborator Author

smmercuri commented Nov 28, 2025

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Nov 28, 2025
@smmercuri
feat(InfinitePlace/Ramification): embeddings of unramified/ramified i…
d4ac089 
…nfinite places satisfy `IsUnmixed/IsMixed` (#29946)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 28, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(InfinitePlace/Ramification): embeddings of unramified/ramified infinite places satisfy IsUnmixed/IsMixed [Merged by Bors] - feat(InfinitePlace/Ramification): embeddings of unramified/ramified infinite places satisfy IsUnmixed/IsMixed Nov 28, 2025
@mathlib-bors mathlib-bors bot closed this Nov 28, 2025
@alexjbest alexjbest removed their assignment Feb 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@riccardobrasca riccardobrasca riccardobrasca approved these changes

+1 more reviewer

@xroblot xroblot xroblot approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). FLT part of the ongoing formalization of Fermat's Last Theorem t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@smmercuri @mathlib4-dependent-issues-bot @mathlib4-merge-conflict-bot @riccardobrasca @xroblot @alexjbest