Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-30 06:04 06b1d878

View on Github →

feat(algebra/group): add commute.is_unit_mul_iff (#10042)

Estimated changes

Modified src/algebra/group/commute.lean

added theorem commute.is_unit_mul_iff

added theorem is_unit_mul_self_iff

Modified src/algebra/group_power/lemmas.lean

modified theorem is_unit_pos_pow_iff

added theorem is_unit_pow_succ_iff