Theorem NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot

Modification history

2026-07-01 13:18
Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean
chore(NumberTheory/NumberField/Units/Basic): use `Nat.card` instead of `Fintype.card` (#41210) …
Modified NumberField.Units.dvd_torsionOrder_of_isPrimitiveRootView on Github →
2025-12-16 10:54
Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean
feat(Cyclotomic): compute the torsion order of a cyclotomic field (#32782) …
Added NumberField.Units.dvd_torsionOrder_of_isPrimitiveRootView on Github →