Theorem IsCyclotomicExtension.union_of_isPrimitiveRoot

Modification history

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