Theorem IsPrimitiveRoot.lcm_totient_le_finrank

Modification history

2024-03-28 10:26
Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
feat: characterize roots of unity in cyclotomic extensions (#10710) …
Added IsPrimitiveRoot.lcm_totient_le_finrankView on Github →