Mathlib Changelog
v4
Changelog
About
Github
Theorem
mul_left_ne_self
Modification history
2023-04-29 16:26
Mathlib/Algebra/Group/Basic.lean
feat: `a * b ≠ b ↔ a ≠ 1` (#3726) …
Added
mul_left_ne_self
View on Github →