Theorem IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity'

Modification history

2024-11-04 08:35

Mathlib/RingTheory/RootsOfUnity/Basic.lean

chore: refactor roots of unity to avoid PNat (#18516) …

Deleted IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity'View on Github →

2024-05-30 13:23

Mathlib/RingTheory/RootsOfUnity/Basic.lean

feat(RingTheory/RootsOfUnity/Basic): add more covenient version of a lemma (#13375) …

Added IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity'View on Github →