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