Commit 2025-12-05 13:19 6de4df16

View on Github →

feat(CMField): add IsCyclotomicExtension.Rat.isCMField (#31812) We remove the NumberField hypothesis in two more results and thus can deduce that any nontrivial cyclotomic extension of ℚ is CM. In particular, we add the instance:

instance (K : Type*) [Field K] [CharZero K] [IsCyclotomicExtension ⊤ ℚ K] : IsCMField K

Estimated changes

Modified Mathlib/NumberTheory/NumberField/CMField.lean

added theorem NumberField.IsCMField.IsCyclotomicExtension.Rat.isCMField

modified theorem NumberField.IsCMField.ofCMExtension

modified theorem NumberField.IsCMField.of_forall_isConj

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

added theorem IsCyclotomicExtension.Rat.isTotallyComplex

modified theorem IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero

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

added theorem NumberField.InfinitePlace.IsComplex.of_comap

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

added theorem NumberField.isTotallyComplex_of_algebra