Theorem inv_inv'
Modification history
2021-10-01 03:25
src/algebra/group_with_zero/basic.lean
refactor(algebra/group_with_zero): rename lemmas to use ₀ instead of ' (#9424) …
Deleted inv_inv'View on Github →2020-06-05 05:31
src/algebra/field.lean
chore(algebra/*): merge `inv_inv''` with `inv_inv'` (#2954)
Modified inv_inv'View on Github →2020-05-18 13:38
src/algebra/field.lean
refactor(algebra): merge init_.algebra into algebra (#2707) …
Modified inv_inv'View on Github →2020-05-17 17:58
src/init_/algebra/field.lean
chore(*): bump to lean-3.13.1 (#2697) …
Added inv_inv'View on Github →2020-03-05 13:17
src/algebra/field.lean
chore(*): switch to lean 3.6.1 (#2064) …
Deleted inv_inv'View on Github →2019-09-27 11:47
src/algebra/field.lean
feat(logic/function): define `function.involutive` (#1474) …
Modified inv_inv'View on Github →2017-09-21 13:22
algebra/group_power.lean
feat(topology/lebesgue_measure): add Lebesgue outer measure; show that the lower half open interval is measurable
Modified inv_inv'View on Github →2017-09-21 10:33
algebra/group_power.lean
Merge branch 'master' of https://github.com/leanprover/mathlib
Modified inv_inv'View on Github →2017-09-20 20:02
topology/ennreal.lean
feat(topology/outer_measure): add outer measures and tools for Caratheodorys extension method
Deleted inv_inv'View on Github →