Commit 2026-09-29 22:08 95dad55a

View on Github →

chore: rename HasEnoughRootsOfUnity.exists_primitiveRoot to exists_isPrimitiveRoot (#44326) Its conclusion is about the predicate IsPrimitiveRoot.

Estimated changes

Modified Mathlib/GroupTheory/FiniteAbelian/Duality.lean

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

Modified Mathlib/RingTheory/RootsOfUnity/EnoughRootsOfUnity.lean

added theorem HasEnoughRootsOfUnity.exists_isPrimitiveRoot

deleted theorem HasEnoughRootsOfUnity.exists_primitiveRoot