English
For a given finite-index family and a family of elements u(i) ∈ H_i, the canonical homomorphism equals the finite product ∏_{i} u(i) with the appropriate shuffling dictated by commutativity.
Русский
Для данного конечного индекса и семейства элементов u(i) ∈ H_i канонический гомоморфизм равен конечному произведению ∏_{i} u(i) с учётом коммютативности.
LaTeX
$$$(\text{noncommPiCoprod }\text{comm})\,u = \operatorname{noncommProd}_{i\in \iota} (u(i))$$$
Lean4
@[to_additive]
theorem noncommPiCoprod_apply (comm) (u : (i : ι) → H i) :
Subgroup.noncommPiCoprod comm u =
Finset.noncommProd Finset.univ (fun i ↦ u i) (fun i _ j _ h ↦ comm h _ _ (u i).prop (u j).prop) :=
by simp only [Subgroup.noncommPiCoprod, MonoidHom.noncommPiCoprod, coe_subtype, MonoidHom.coe_mk, OneHom.coe_mk]
