English
There is a linear equivalence between the product of two linear maps and the linear map into a product of codomains, identifying (f,g) ↦ f.prod g with its inverse using fst and snd.
Русский
Существует линейное эквивалентное отображение между произведением двух линейных отображений и линейным отображением в произведение кодоменов, идентифицируя (f,g) ↦ f.prod g и его обратное через fst и snd.
LaTeX
$$$\text{prodEquiv}: (M\to_{{R}} M_2) \times (M\to_{{R}} M_3) \cong_{{S}} M \to_{{R}} (M_2 \times M_3)$ with explicit toFun$x\mapsto x.1.prod x.2$ and invFun$f\mapsto (fst\, f, snd\, f)$.$$
Lean4
@[simp]
theorem pair_fst_snd : prod (fst R M M₂) (snd R M M₂) = LinearMap.id :=
rfl
