congr_tprod — Mathlib

English

If f_i : s_i → t_i → t'_i are linear maps, then map₂ applied to tprod R x, tprod R y yields tprod R (λ i, f_i(x_i)(y_i)).

Русский

Если f_i : s_i → t_i → t'_i — линейные отображения, то map₂ применяется к tprod x, tprod y даёт tprod (λi, f_i(x_i)(y_i)).

LaTeX

$$$\mathrm{map}_2\ f\ (\,tprod\ R x)\ (tprod\ R y) = tprod\ R (\lambda i. f_i(x_i)(y_i))$$$

Lean4

@[simp]
theorem congr_tprod (f : Π i, s i ≃ₗ[R] t i) (m : Π i, s i) :
    congr f (tprod R m) = tprod R (fun (i : ι) ↦ (f i) (m i)) := by
  simp only [congr, LinearEquiv.ofLinear_apply, map_tprod, LinearEquiv.coe_coe]

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