Commit 2024-03-01 13:29 267bced6

View on Github →

feat: cyclotomic fields are totally complex (#10502) We prove that cyclotomic fields are totally complex. From flt-regular.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Cyclotomic/Embeddings.lean

added theorem IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two

added theorem IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt

added theorem NumberField.InfinitePlace.nrComplexPlaces_eq_zero_of_finrank_eq_one

added theorem NumberField.InfinitePlace.nrRealPlaces_eq_one_of_finrank_eq_one