commSemigroup — Mathlib

English

With the product S * T defined by { xy | x ∈ S, y ∈ T }, LowerSet α forms a commutative semigroup under multiplication.

Русский

Для LowerSet α при заданном произведении S * T = { xy | x ∈ S, y ∈ T } множествоLowerSet образует коммутативную полугруппу по умножению.

LaTeX

$$LowerSet α forms a CommSemigroup under the product S * T := { xy : x ∈ S, y ∈ T }$$

Lean4

@[to_additive]
instance commSemigroup : CommSemigroup (LowerSet α) :=
  { (SetLike.coe_injective.commSemigroup _ coe_mul : CommSemigroup (LowerSet α)) with }

Похожие утверждения