Theorem IsPrimitiveRoot.prod_pow_sub_one_eq_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.prod_pow_sub_one_eq_orderView on Github →