Def OrderedCommGroup.mkOfCone

Modification history

2025-04-10 16:38

Mathlib/Algebra/Order/Group/Cone.lean

chore: deprecate semibundled ordered algebraic typeclasses (#20676) …

Deleted OrderedCommGroup.mkOfCone View on Github →

2024-09-05 15:25

Mathlib/Algebra/Order/Group/Cone.lean

feat(Algebra/Order): rewrite positive cones to use substructure pattern (#15975) …

Added OrderedCommGroup.mkOfCone View on Github →