Commit 2026-03-21 05:43 e5cf50d7

View on Github →

feat(NumberField/InfinitePlace/Ramification): add cardinality results for (un)ramified places over (#36353) The number of unramified/ramified places over a fixed infinite place v is equal/twice the number of unmixed/mixed complex embeddings over v.embedding

Estimated changes

Modified Mathlib/Data/Set/Card.lean

added theorem Set.ncard_sumEquiv_symm_apply

Modified Mathlib/Logic/Basic.lean

added theorem Function.Injective.ite

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean

added theorem NumberField.ComplexEmbedding.LiesOver.over_apply

added theorem NumberField.ComplexEmbedding.liesOver_iff

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

added theorem NumberField.InfinitePlace.IsRamified.liesOver_isReal_under

added theorem NumberField.InfinitePlace.IsUnramified.liesOver_isReal_over

added theorem NumberField.InfinitePlace.bijOn_sumElim_conjugate

modified theorem NumberField.InfinitePlace.conjugate_embedding_mem_mixedEmbeddingsOver

modified theorem NumberField.InfinitePlace.disjoint_ramifiedPlacesOver_unramifiedPlacesOver

modified theorem NumberField.InfinitePlace.embedding_mem_mixedEmbeddingsOver

modified theorem NumberField.InfinitePlace.liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver

modified theorem NumberField.InfinitePlace.liesOver_embedding_of_mem_ramifiedPlacesOver

modified theorem NumberField.InfinitePlace.mk_mem_ramifiedPlacesOver

modified theorem NumberField.InfinitePlace.mk_mem_unramifiedPlacesOver

modified def NumberField.InfinitePlace.placesOver

modified def NumberField.InfinitePlace.ramifiedPlacesOver

added theorem NumberField.InfinitePlace.ramifiedPlacesOver_ncard

modified theorem NumberField.InfinitePlace.union_ramifiedPlacesOver_unramifiedPlacesOver

added theorem NumberField.InfinitePlace.unramifedPlacesOver_ncard_add_eq_finrank

modified def NumberField.InfinitePlace.unramifiedPlacesOver

added theorem NumberField.InfinitePlace.unramifiedPlacesOver_ncard