rTensorHomEquivHomRTensor_apply — Mathlib

English

The rtensor-hom equivalence, when applied to elements, matches the standard rtensor-hom map.

Русский

Применение эквивалентности rtensor-гом к элементам совпдает с обычной картой rtensor-гом.

LaTeX

$$$\\big(rTensorHomEquivHomRTensor\\;R\\;M\\;P\\;Q\\big).toLinearMap(x) = rTensorHomToHomRTensor\\;R\\;M\\;P\\;Q\\;x$$$

Lean4

@[simp]
theorem rTensorHomEquivHomRTensor_apply (x : (M →ₗ[R] P) ⊗[R] Q) :
    rTensorHomEquivHomRTensor R M P Q x = rTensorHomToHomRTensor R M P Q x := by
  rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap]

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