Theorem Nonneg.inv_mk

Modification history

2024-07-17 17:39
Mathlib/Algebra/Order/Nonneg/Field.lean
chore (Algebra.Order.Field.Defs): split off results about unbundled ordered algebra (#14451) …
Modified Nonneg.inv_mkView on Github →
2023-02-11 20:43
Mathlib/Algebra/Order/Nonneg/Field.lean
feat: port Algebra.Order.Nonneg.Field (#2200)
Added Nonneg.inv_mkView on Github →