Commit 2025-07-11 22:12 ba454ce1

View on Github →

feat(NumberField/CMField): A totally complex abelian extension of ℚ is CM (#26073) This PR continues the work from #25619. Original PR: https://github.com/leanprover-community/mathlib4/pull/25619

depends on: #25818

Estimated changes

Modified Mathlib/FieldTheory/Galois/Basic.lean

added def IntermediateField.subgroupEquivAlgEquiv

Modified Mathlib/NumberTheory/NumberField/CMField.lean

added theorem NumberField.IsCMField.of_forall_isConj

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

added theorem NumberField.ComplexEmbedding.IsConj.comp

added theorem NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one