instCommMonoidCoeOfSubmonoidClass

English

If each fiber is a Commutative Monoid, the restricted product is a Commutative Monoid with coordinatewise addition/multiplication: the operations commute coordinatewise.

Русский

Если каждый элемент — коммутативный моноид, ограниченное произведение является коммутативным моноидом с координатной реализацией операций.

LaTeX

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

Lean4

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

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