English
The collection of convex cones in a fixed module M over a semiring R forms an additive commutative semigroup under Minkowski (cone) addition; in particular, the sum of two convex cones is again a convex cone, addition is associative, and is commutative.
Русский
Множество выпуклых конусов в фиксированном модуле M над полуприведенным полем образует коммутативную полугруппу под операцией Minkowski-суммы; сумма двух конусов снова является выпуклым конусом, сложение ассоциативно и коммутативно.
LaTeX
$$$(\\mathrm{ConvexCone}(R,M), +)$ является коммутативной полугруппой (с операцией Minkowski-суммирования).$$$
Lean4
instance instAddCommSemigroup : AddCommSemigroup (ConvexCone R M)
where
add := Add.add
add_assoc _ _ _ := SetLike.coe_injective <| add_assoc _ _ _
add_comm _ _ := SetLike.coe_injective <| add_comm _ _
