Theorem IsPrimitiveRoot.associated_pow_add_sub_sub_one

Modification history

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