toMonoid — Mathlib

English

There is a canonical Monoid structure on any submonoid of a Monoid M, inherited from M.

Русский

У любого подмонойда подмножества Monoid M существует каноническая моноидная структура, наследуемая от M.

LaTeX

$$$\mathrm{Submonoid}\;M \text{ has a Monoid structure inherited from } M$$$

Lean4

/-- A submonoid of a monoid inherits a monoid structure. -/
@[to_additive /-- An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure. -/
    ]
instance toMonoid {M : Type*} [Monoid M] (S : Submonoid M) : Monoid S :=
  fast_instance%Subtype.coe_injective.monoid Subtype.val rfl (fun _ _ => rfl) fun _ _ => rfl

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