instCommGroupCoeOfSubgroupClass — Mathlib

English

If each fiber is a Group and the fibers form a Subgroup, the restricted product is a Group with coordinatewise group operation.

Русский

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

LaTeX

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

Lean4

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

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