mathlib3
e4c64493 - feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043)

Commit
3 years ago
feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043) Since it's a bit of a hassle to rewrite `add_mem_iff_left` and `add_mem_iff_right` to subtraction, I made a new pair of lemmas.
Author
Parents
Loading