[Merged by Bors] - feat(NumberField/InfinitePlace/Ramification): add `placesOver` by smmercuri · Pull Request #36132 · leanprover-community/mathlib4

smmercuri · 2026-03-04T13:16:50Z

This PR defines sets of infinite places of L that lie above a fixed infinite place v of K, as well as subsets of ramified/unramified such places.
Also define analogous concepts for complex embeddings.
Fix order of parameters in ComplexEmbedding.LiesOver to match the order of params in AbsoluteValue.LiesOver make it protected.

github-actions · 2026-03-04T13:17:58Z

PR summary 1dc478f792

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ coe_mk_comp
+ conjugate_embedding_mem_mixedEmbeddingsOver
+ disjoint_ramifiedPlacesOver_unramifiedPlacesOver
+ disjoint_unmixedEmbeddingsOver_mixedEmbeddingsOver
+ embedding_mem_mixedEmbeddingsOver
+ instance {φ : K →+* ℂ} {ψ : L →+* ℂ} [ComplexEmbedding.LiesOver ψ φ] :
+ liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver
+ liesOver_embedding_of_mem_ramifiedPlacesOver
+ mixedEmbeddingsOver
+ mk_mem_ramifiedPlacesOver
+ mk_mem_unramifiedPlacesOver
+ placesOver
+ ramifiedPlacesOver
+ union_ramifiedPlacesOver_unramifiedPlacesOver
+ union_unmixedEmbeddingsOver_mixedEmbeddingsOver
+ unmixedEmbeddingsOver
+ unramifiedPlacesOver
++-- LiesOver
- LiesOver.comp_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

riccardobrasca · 2026-03-04T13:29:31Z

@xroblot can you have a look?

riccardobrasca · 2026-03-04T13:29:41Z

(there is a building error btw)

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

Co-authored-by: Laurance Lau <[email protected]>

riccardobrasca · 2026-03-05T13:18:47Z

Thanks!

bors d+

mathlib-bors · 2026-03-05T13:18:49Z

✌️ 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.

…nfinitePlacesOver

smmercuri · 2026-03-05T14:16:12Z

bors r+

- This PR defines sets of infinite places of `L` that lie above a fixed infinite place `v` of `K`, as well as subsets of ramified/unramified such places. - Also define analogous concepts for complex embeddings. - Fix order of parameters in `ComplexEmbedding.LiesOver` to match the order of params in `AbsoluteValue.LiesOver` make it protected.

mathlib-bors · 2026-03-05T15:09:40Z

Pull request successfully merged into master.

Build succeeded:

…rover-community#36132) - This PR defines sets of infinite places of `L` that lie above a fixed infinite place `v` of `K`, as well as subsets of ramified/unramified such places. - Also define analogous concepts for complex embeddings. - Fix order of parameters in `ComplexEmbedding.LiesOver` to match the order of params in `AbsoluteValue.LiesOver` make it protected.

add placesOver

c9ee1ff

smmercuri requested a review from riccardobrasca March 4, 2026 13:19

smmercuri mentioned this pull request Mar 4, 2026

feat: NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank #30551

Open

9 tasks

riccardobrasca self-assigned this Mar 4, 2026

smmercuri added the FLT part of the ongoing formalization of Fermat's Last Theorem label Mar 4, 2026

add protected and fix build

6d8ffab

LLaurance reviewed Mar 5, 2026

View reviewed changes