map₂_tprod_tprod — Mathlib

English

piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) equals tprod R (λ i, f_i(a_i)(b_i)).

Русский

piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (λ i, f_i(a_i)(b_i)).

LaTeX

$$$\pi TensorHomMap_2 (tprod\ R\ f)\ (tprod\ R\ a)\ (tprod\ R\ b) = tprod\ R (\lambda i. f_i(a_i)(b_i))$$$

Lean4

theorem map₂_tprod_tprod (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) (x : Π i, s i) (y : Π i, t i) :
    map₂ f (tprod R x) (tprod R y) = tprod R fun i ↦ f i (x i) (y i) := by simp [map₂]

Похожие утверждения