Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-13 15:08 e6819d3a

View on Github →

feat(algebra/group_power/lemmas): add invertible_of_pow_eq_one (#6658)

Estimated changes

Modified src/algebra/associated.lean

deleted theorem is_unit.pow

Modified src/algebra/group_power/lemmas.lean

added def invertible_of_pow_eq_one

added def invertible_of_pow_succ_eq_one

added theorem is_unit.pow