piTensorHomMapFun₂_smul — Mathlib

English

piTensorHomMap₂ is the canonical linear map sending tensors of linear maps to a linear map between tensor products.

Русский

piTensorHomMap₂ — каноническое линейное отображение, переводящее тензоры линейных отображений в линейное отображение между тензорными произведениями.

LaTeX

$$$\pi\text{TensorHomMap}_2 : (\otimes_i s_i \to s_i) \to (\otimes_i t_i) \to (\otimes_i t'_i)$$$

Lean4

theorem piTensorHomMapFun₂_smul (r : R) (φ : ⨂[R] i, s i →ₗ[R] t i →ₗ[R] t' i) :
    piTensorHomMapFun₂ (r • φ) = r • piTensorHomMapFun₂ φ := by dsimp [piTensorHomMapFun₂]; ext;
  simp only [map_smul, LinearMap.compMultilinearMap_apply, lift.tprod, smul_apply, LinearMap.smul_apply]

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