Commit 2024-02-15 20:02 c5234383

View on Github →

chore: Golf exists_pow_eq_one_of_zpow_eq_one (#10559) and replace it by two more explicit lemmas

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

deleted theorem exists_npow_eq_one_of_zpow_eq_one

added theorem exists_pow_eq_one_of_zpow_eq_one

added theorem pow_natAbs_eq_one

Modified Mathlib/Algebra/Module/Torsion.lean

Modified Mathlib/Data/Int/Order/Basic.lean

added theorem zpow_abs_eq_one