Mathlib v3 is deprecated. Go to Mathlib v4

Theorem inv_eq_zero

Modification history

2020-04-06 23:05
src/algebra/field.lean
feat(algebra/group_with_zero): groups with a zero element adjoined (#2242) …
Modified inv_eq_zeroView on Github →
2019-07-30 06:58
src/algebra/field.lean
feat(algebra,data/complex/exponential): add abs_neg_one_pow, remove hyp from div_le_div_of_le_left (#1280)
Modified inv_eq_zeroView on Github →
2019-03-27 21:47
src/algebra/field.lean
feat(algebra/field_power): add fpow_one, one_fpow, fpow_mul, mul_fpow (closes #855)
Modified inv_eq_zeroView on Github →
2019-03-17 09:07
src/algebra/field.lean
feat(order/filter/filter_product): build hyperreals (#801) …
Modified inv_eq_zeroView on Github →
2018-08-21 22:05
data/real/nnreal.lean
refactor(data/real/nnreal): derive order structure for ennreal from with_top nnreal
Added inv_eq_zeroView on Github →