mathlib3
c8771b6b
- fix(algebra/ring/basic): delete mul_self_sub_mul_self_eq (#4119)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
fix(algebra/ring/basic): delete mul_self_sub_mul_self_eq (#4119) It's redundant with `mul_self_sub_mul_self`. Also renamed `mul_self_sub_one_eq` to `mul_self_sub_one`.
References
#4925 - Make prime-avoidance branch build
Author
bryangingechen
Parents
169384a7
Loading