instMonoidCoeOfSubmonoidClass — Mathlib

English

The restricted product inherits a Monoid structure; the product operation is defined coordinatewise: (x · y)_i = x_i · y_i.

Русский

Ограниченное произведение наследует моноидовую структуру; операция произведения по координатам: (x · y)_i = x_i · y_i.

LaTeX

$$$ (x y)_i = x_i y_i \quad (\forall i). $$$

Lean4

@[to_additive]
instance [Π i, Monoid (R i)] [∀ i, SubmonoidClass (S i) (R i)] : Monoid (Πʳ i, [R i, B i]_[𝓕]) :=
  DFunLike.coe_injective.monoid _ rfl (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

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