lTensor_comp — Mathlib

English

The left-tensor functor is compatible with composition of linear maps: lTensor(A, M, f2 ∘ f1) = (lTensor(A, M, f2)) ∘ (lTensor(A, M, f1)).

Русский

Левый тензорный функтор корректно переносиет композицию линейных отображений: lTensor(A, M, f2 ∘ f1) = (lTensor(A, M, f2)) ∘ (lTensor(A, M, f1)).

LaTeX

$$$\\mathrm{lTensor}(A, M, f_2 \\circ f_1) = \\big(\\mathrm{lTensor}(A, M, f_2)\\big) \\circ \\big(\\mathrm{lTensor}(A, M, f_1)\\big).$$$

Lean4

theorem lTensor_comp (f₂ : Q →ₗ[R] Q') (f₁ : N →ₗ[R] Q) :
    lTensor A M (f₂.comp f₁) = (lTensor A M f₂).comp (lTensor A M f₁) :=
  ext fun _ _ => rfl

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