Mathlib v3 is deprecated. Go to Mathlib v4

Theorem one_div

Modification history

2021-01-02 00:36
src/algebra/group/basic.lean
chore(algebra/*): move some lemmas to `div_inv_monoid` (#5552)
Modified one_divView on Github →
2020-12-11 13:45
src/algebra/group_with_zero/basic.lean
chore(*): don't assume `sub_eq_add_neg` and `div_eq_mul_inv` are defeq (#5302) …
Modified one_divView on Github →
2020-08-13 06:22
src/algebra/group_with_zero.lean
fix(algebra/field) remove `one_div_eq_inv` (#3749) …
Modified one_divView on Github →
2020-04-06 23:05
src/algebra/group_with_zero.lean
feat(algebra/group_with_zero): groups with a zero element adjoined (#2242) …
Added one_divView on Github →