Commit 2023-04-28 17:05 84771a9f
View on Github →feat(algebra/group/basic): a * b ≠ b ↔ a ≠ 1 (#18635)
A few convenient corollaries of existing lemmas and a / 2 ≤ a ↔ 0 ≤ a.
feat(algebra/group/basic): a * b ≠ b ↔ a ≠ 1 (#18635)
A few convenient corollaries of existing lemmas and a / 2 ≤ a ↔ 0 ≤ a.