Theorem IsCyclotomicExtension.Rat.torsionOrder_eq

Modification history

2025-12-16 10:54
Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean
feat(Cyclotomic): compute the torsion order of a cyclotomic field (#32782) …
Added IsCyclotomicExtension.Rat.torsionOrder_eqView on Github →