mathlib
386962c2
- feat(algebra/char_zero): `neg_eq_self_iff` (#7916)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
feat(algebra/char_zero): `neg_eq_self_iff` (#7916) `-a = a ↔ a = 0` and `a = -a ↔ a = 0`.
Author
benjamindavidson
Parents
461b444d
Loading