smul_lTensor — Mathlib

English

The identities linking lTensor and rTensor with TensorProduct.comm hold, expressing compatibilities of swapping factors.

Русский

Связи между lTensor и rTensor с TensorProduct.comm выражают совместимость обмена множителей.

LaTeX

$$$ TensorProduct.comm R P Q \\circ lTensor Q g \\circ TensorProduct.comm R N Q = rTensor Q g $$$

Lean4

theorem smul_lTensor {S : Type*} [CommSemiring S] [SMul R S] [Module S M] [IsScalarTower R S M] [SMulCommClass R S M]
    (s : S) (m : M ⊗[R] N) : s • (f.lTensor M) m = (f.lTensor M) (s • m) :=
  have h : s • (f.lTensor M) = f.lTensor M ∘ₗ (LinearMap.lsmul S (M ⊗[R] N) s).restrictScalars R :=
    TensorProduct.ext rfl
  congrFun (congrArg DFunLike.coe h) m

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