Theorem IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver'

Modification history

2025-10-29 08:27
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
chore(NumberField/Cyclotomic): add statements for the case of power one (#30996)
Added IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver'View on Github →