Theorem div_eq_mul_inv
Modification history
2022-05-05 23:51
src/algebra/group/defs.lean
feat(algebra/group/defs): Division monoids (#13860) …
Modified div_eq_mul_invView on Github →2020-12-16 15:31
src/algebra/group/defs.lean
chore(*): add a `div`/`sub` field to (`add_`)`group`(`_with_zero`) (#5303) …
Modified div_eq_mul_invView 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 div_eq_mul_invView on Github →2020-07-01 23:16
src/algebra/group_with_zero.lean
chore(algebra/*): deduplicate `*_with_zero`/`semiring`/`field` (#3259) …
Modified div_eq_mul_invView on Github →2020-04-06 23:05
src/algebra/field.lean
feat(algebra/group_with_zero): groups with a zero element adjoined (#2242) …
Modified div_eq_mul_invView on Github →2018-01-14 21:59
algebra/field.lean
feat(algebra/field): more division lemmas
Modified div_eq_mul_invView on Github →2017-09-28 19:16
algebra/ring.lean
chore(topology): move general theorems to the corresponding theories
Modified div_eq_mul_invView on Github →2017-09-21 13:22
topology/limits.lean
feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable
Added div_eq_mul_invView on Github →