Commit 2025-02-04 15:53 bb2bafa0

View on Github →

chore: rename isUnit_ofPowEqOne (#21407) Units.ofPowEqOne is not present in the signature.

Estimated changes

Modified Mathlib/Algebra/Group/Commute/Units.lean

added theorem IsUnit.of_pow_eq_one

deleted theorem isUnit_ofPowEqOne

Modified Mathlib/Algebra/Polynomial/UnitTrinomial.lean

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean