Def LinearOrderedAddCommGroup.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 LinearOrderedAddCommGroup.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 LinearOrderedAddCommGroup.mkOfPositiveConeView on Github →