Theorem IsPrimitiveRoot.self_sub_one_pow_dvd_order

Modification history

2024-05-28 11:56
Mathlib/RingTheory/RootsOfUnity/Lemmas.lean
feat(RingTheory/RootsOfUnity): product representation of the order of a primitive root of unity (#13290) …
Added IsPrimitiveRoot.self_sub_one_pow_dvd_orderView on Github →