mathlib3
5cafdfff
- chore(algebra/group/basic): dedup, add a lemma (#6810)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
chore(algebra/group/basic): dedup, add a lemma (#6810) * drop `sub_eq_zero_iff_eq`, was a duplicate of `sub_eq_zero`; * add a `simp` lemma `sub_eq_self : a - b = a ↔ b = 0`.
Author
urkud
Parents
94f59d8b
Loading