lTensorHomEquivHomLTensor_apply — Mathlib

English

For x in P ⊗_R (M →_R Q), applying the LTensor-Hom LTensor equivalence matches the direct LTensor-Hom LTensor construction.

Русский

Для x в P ⊗_R (M →_R Q) отображение через эквивалентность совпадает с прямым конструктором LTensor-Hom LTensor.

LaTeX

$$$(lTensorHomEquivHomLTensor\\;R\\;M\\;P\\;Q)(x) = lTensorHomToHomLTensor\\;R\\;M\\;P\\;Q\\;x$$$

Lean4

@[simp]
theorem lTensorHomEquivHomLTensor_apply (x : P ⊗[R] (M →ₗ[R] Q)) :
    lTensorHomEquivHomLTensor R M P Q x = lTensorHomToHomLTensor R M P Q x := by
  rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]

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