English
There is a linear equivalence between the product of maps and maps out of the product, given by f ↦ (f₁.coprod f₂) with inverse given by composing with inl and inr.
Русский
Существует линейное эквивалентное соответствие между произведением отображений и отображениями из произведения, заданное через coprod соотношение и обратное посредством композиции с inl и inr.
LaTeX
$$$ coprodEquiv [Module S M_3] [SMulCommClass R S M_3] : ((M \\to[M_3]) \\times (M_2 \\to M_3)) \\simeq_ℒ[S] (M \\times M_2) \\to M_3 $$$
Lean4
/-- Split equality of linear maps from a product into linear maps over each component, to allow `ext`
to apply lemmas specific to `M →ₗ M₃` and `M₂ →ₗ M₃`.
See note [partially-applied ext lemmas]. -/
@[ext 1100]
theorem prod_ext {f g : M × M₂ →ₗ[R] M₃} (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
(hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) : f = g :=
prod_ext_iff.2 ⟨hl, hr⟩
