instGroupCoeOfSubgroupClass — Mathlib

English

The restricted product supports integer scalar multiplication in a coordinatewise way when fibers are additive submonoids; zsmul acts componentwise.

Русский

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

LaTeX

$$$ (n \cdot x)_i = n \cdot x_i \quad (i). $$$

Lean4

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

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