English
Let f: M → M3 and g: M2 → M4 be linear maps. The prodMap of f and g corresponds to applying f to the first component and g to the second component; equivalently, the underlying function of f.prodMap g is the same as the standard product map (f, g).
Русский
Пусть f: M → M3 и g: M2 → M4 — линейные отображения. Отображение-prodMap f g действует на пару (m, n) как (f(m), g(n)); соответственно, базовое отображение, лежащее в основе f.prodMap g, совпадает с обычным отображением в произведение (f, g).
LaTeX
$$$ (f \\text{ prodMap } g)(m, n) = (f(m),\\, g(n)). $$$
Lean4
theorem coe_prodMap (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : ⇑(f.prodMap g) = Prod.map f g :=
rfl
