English
For a finite index set ι and a family G = (G_i), the canonical additive isomorphism between the finite direct sum ⨁_{i∈ι} G_i and the product ∏_{i∈ι} G_i exists.
Русский
Для конечного множества индексов ι и семейства групп G = (G_i) существует канонический аддитивный изоморфизм между конечной прямой суммой ⨁_{i∈ι} G_i и произведением ∏_{i∈ι} G_i.
LaTeX
$$$\DirectSum ι G \;\cong_+\; \prod_{i\in ι} G_i$$$
Lean4
/-- The canonical isomorphism of a finite direct sum of additive commutative monoids
and the corresponding finite product. -/
def addEquivProd {ι : Type*} [Fintype ι] (G : ι → Type*) [(i : ι) → AddCommMonoid (G i)] :
DirectSum ι G ≃+ ((i : ι) → G i) :=
⟨DFinsupp.equivFunOnFintype, fun g h ↦
funext fun _ ↦ by
simp only [DFinsupp.equivFunOnFintype, Equiv.toFun_as_coe, Equiv.coe_fn_mk, add_apply, Pi.add_apply]⟩
