Commit 2025-12-12 08:03 f6835d4d

View on Github →

feat: strengthen pow_gcd_eq_one (#32464) From ClassFieldTheory

Estimated changes

Modified Mathlib/Data/Int/GCD.lean

added theorem pow_eq_one_iff_of_coprime

modified theorem pow_gcd_eq_one

added theorem pow_intGCD_eq_one

Modified Mathlib/Data/Int/Init.lean

added theorem Int.gcd_negSucc_negSucc

added theorem Int.gcd_negSucc_ofNat

added theorem Int.gcd_ofNat_negSucc

Modified Mathlib/GroupTheory/OrderOfElement.lean

modified theorem pow_gcd_card_eq_one_iff

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean