piTensorHomMap₂_tprod_tprod_tprod

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

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

Lean4

@[simp]
theorem piTensorHomMap₂_tprod_tprod_tprod (f : ∀ i, s i →ₗ[R] t i →ₗ[R] t' i) (a : ∀ i, s i) (b : ∀ i, t i) :
    piTensorHomMap₂ (tprod R f) (tprod R a) (tprod R b) = tprod R (fun i ↦ f i (a i) (b i)) := by
  simp [piTensorHomMapFun₂, piTensorHomMap₂]

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