Theorem IsPrimitiveRoot.«exists»

Modification history

2025-02-16 10:26

Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

chore(RingTheory): golf `IsPrimitiveRoot.exists_pos` (#21937)

Deleted IsPrimitiveRoot.«exists»View on Github →

2025-02-14 19:33

Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

feat(RingTheory): frobenius elements (#21770)

Added IsPrimitiveRoot.«exists»View on Github →