toCommMonoid — Mathlib

English

A submonoid of a commutative monoid is itself a commutative monoid.

Русский

Подмножество подмономиода коммутативного моноида само образует коммутативный моноид.

LaTeX

$$$\mathrm{Submonoid}\;M \text{ in a CommMonoid } M \text{ inherits a CommMonoid structure}$$$

Lean4

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

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