Commit 2025-10-29 08:27 f45bc7ab

View on Github →

chore(NumberField/Cyclotomic): add statements for the case of power one (#30996)

Estimated changes

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

added theorem IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver'

added theorem IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime

added theorem IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'

added theorem IsCyclotomicExtension.Rat.ncard_primesOver_of_prime

added theorem IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime

added theorem IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one'