Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-16 16:01 b2b0de46

View on Github →

feat(algebra/group/basic): mul_left_eq_self etc (#1446) Simp-lemmas for groups of the form a * b = b ↔ a = 1.

Estimated changes