basic): `a * b ≠ b ↔ a ≠ 1` (#18635)

Commit

2 years ago

feat(algebra/group/basic): `a * b ≠ b ↔ a ≠ 1` (#18635) A few convenient corollaries of existing lemmas and `a / 2 ≤ a ↔ 0 ≤ a`.

Author

YaelDillies

Parents