Commit 2021-03-23 15:29 5cafdfff
View on Github →chore(algebra/group/basic): dedup, add a lemma (#6810)
- drop
sub_eq_zero_iff_eq, was a duplicate ofsub_eq_zero; - add a
simplemmasub_eq_self : a - b = a ↔ b = 0.
chore(algebra/group/basic): dedup, add a lemma (#6810)
sub_eq_zero_iff_eq, was a duplicate of sub_eq_zero;simp lemma sub_eq_self : a - b = a ↔ b = 0.