Theorem IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one'

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.ramificationIdx_span_zeta_sub_one'View on Github →