Theorem IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime

Modification history

2025-10-15 16:18
Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean
feat: add Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits (#30085) …
Added IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprimeView on Github →