Theorem IsPrimitiveRoot.toInteger_sub_one_dvd_prime'

Modification history

2024-05-15 19:02
Mathlib/NumberTheory/Cyclotomic/Rat.lean
feat(Mathlib.NumberTheory.FLT.Three): add `FermatLastTheoremForThree_of_FermatLastTheoremThreeGen` (#12767) …
Added IsPrimitiveRoot.toInteger_sub_one_dvd_prime'View on Github →