feat: a * b ≠ b ↔ a ≠ 1 (#3726) https://github.com/leanprover-community/mathlib/pull/18635
a * b ≠ b ↔ a ≠ 1
algebra.group.basic
2196ab363eb097c008d4497125e0dde23fb36db2
84771a9f5f0bd5e5d6218811556508ddf476dcbd
algebra.order.field.basic
44e29dbcff83ba7114a464d592b8c3743987c1e5