Commit 2024-02-25 22:36 61dc2d08

View on Github →

chore(Algebra/Order/Group): move PositiveCones to a new file (#10868) Nothing else in the library (but a similar file about rings) depend on these constructors.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Group/Cone.lean

added structure AddCommGroup.PositiveCone

added structure AddCommGroup.TotalPositiveCone

added def LinearOrderedAddCommGroup.mkOfPositiveCone

added def OrderedAddCommGroup.mkOfPositiveCone

Modified Mathlib/Algebra/Order/Group/Defs.lean

deleted structure AddCommGroup.PositiveCone

deleted structure AddCommGroup.TotalPositiveCone

deleted def LinearOrderedAddCommGroup.mkOfPositiveCone

deleted def OrderedAddCommGroup.mkOfPositiveCone

Modified Mathlib/Algebra/Order/Ring/Cone.lean