mathlib
6c8b2cd6
- fix(algebra/field) remove `one_div_eq_inv` (#3749)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
fix(algebra/field) remove `one_div_eq_inv` (#3749) It already existed as `one_div` for `group_with_zero` Also make `one_div` a `simp` lemma and renamed `nnreal.one_div_eq_inv` to `nnreal.one_div`.
Author
fpvandoorn
Parents
d6ffc1ad
Loading