Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-16 10:26
c6b3ead1
View on Github →
chore(RingTheory): golf
IsPrimitiveRoot.exists_pos
(
#21937
)
Estimated changes
Modified
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
deleted
theorem
IsPrimitiveRoot.«exists»