Mathlib Changelog
v4
Changelog
About
Github
Theorem
mul_right_ne_self
Modification history
2025-03-13 23:54
Mathlib/Algebra/Group/Basic.lean
chore(Algebra/Group/Basic): rename mul_right_eq_self to mul_eq_left etc (#22587) …
Deleted
mul_right_ne_self
View on Github →
2023-04-29 16:26
Mathlib/Algebra/Group/Basic.lean
feat: `a * b ≠ b ↔ a ≠ 1` (#3726) …
Added
mul_right_ne_self
View on Github →