Def OrderedAddCommGroup.mkOfPositiveCone

Modification history

2024-09-05 15:25
Mathlib/Algebra/Order/Group/Cone.lean
feat(Algebra/Order): rewrite positive cones to use substructure pattern (#15975) …
Deleted OrderedAddCommGroup.mkOfPositiveConeView on Github →
2024-02-25 22:36
Mathlib/Algebra/Order/Group/Cone.lean
chore(Algebra/Order/Group): move `PositiveCone`s to a new file (#10868) …
Modified OrderedAddCommGroup.mkOfPositiveConeView on Github →
2023-08-10 19:52
Mathlib/Algebra/Order/Group/Defs.lean
chore: banish `Type _` and `Sort _` (#6499) …
Modified OrderedAddCommGroup.mkOfPositiveConeView on Github →
2022-12-06 13:59
Mathlib/Algebra/Order/Group/Defs.lean
feat: port algebra.order.group.defs (#869) …
Added OrderedAddCommGroup.mkOfPositiveConeView on Github →