piTensorHomMap_tprod_tprod — Mathlib

English

For h a multilinear map t → E, lift h composed with map f equals lift of h after composing linearly with f: lift h ∘ map f = lift (h.compLinearMap f).

Русский

Пусть h — мультилейная, тогда композиция lift h с map f равна подъему h после линейной композиции с f.

LaTeX

$$$\mathrm{lift}\, h \circ_\ell \mathrm{map}\, f = \mathrm{lift}\, (h \circ_{\text{LinearMap}} f)$$$

Lean4

@[simp]
theorem piTensorHomMap_tprod_tprod (f : Π i, s i →ₗ[R] t i) (x : Π i, s i) :
    piTensorHomMap (tprod R f) (tprod R x) = tprod R fun i ↦ f i (x i) := by simp [piTensorHomMap]

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