Theorem HasEnoughRootsOfUnity.exists_primitiveRoot

Modification history

2026-09-29 22:08
Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean
chore: rename `HasEnoughRootsOfUnity.exists_primitiveRoot` to `exists_isPrimitiveRoot` (#44326) …
Deleted HasEnoughRootsOfUnity.exists_primitiveRootView on Github →
2024-11-06 07:46
Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean
feat(RingTheory/RootsOfUnity/EnoughRootsOfUnity): new file (#18681) …
Added HasEnoughRootsOfUnity.exists_primitiveRootView on Github →