toCommMonoid — Mathlib

English

A submonoid of a commutative monoid inherits a commutative monoid structure.

Русский

Подмономиод коммутативного моноида наследует коммутативную моноидную структуру.

LaTeX

$$$ \text{CommMonoid}(\text{Subtype} S) \quad \text{(из подмономиода S внутри коммутативного моноида)} $$$

Lean4

/-- A submonoid of a `CommMonoid` is a `CommMonoid`. -/
@[to_additive /-- An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`. -/
    ]
instance (priority := 75) toCommMonoid {M} [CommMonoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) :
    CommMonoid S :=
  fast_instance%Subtype.coe_injective.commMonoid Subtype.val rfl (fun _ _ => rfl) fun _ _ => rfl

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