English
The isomorphism homTensorHomEquiv is compatible with the underlying linear maps; i.e., it is equal to the corresponding toLinearMap.
Русский
Изоморфизм homTensorHomEquiv совместим с соответствующими линейными отображениями; тождественен соответствующему toLinearMap.
LaTeX
$$$\\text{Eq}((\\mathrm{homTensorHomEquiv}\\;R\\;M\\;N\\;P\\;Q).toLinearMap, \\; \\mathrm{homTensorHomMap}\\;R\\;M\\;N\\;P\\;Q)$$$
Lean4
@[simp]
theorem homTensorHomEquiv_toLinearMap : (homTensorHomEquiv R M N P Q).toLinearMap = homTensorHomMap R M N P Q :=
by
ext m n
simp only [homTensorHomEquiv, compr₂_apply, mk_apply, LinearEquiv.coe_toLinearMap, LinearEquiv.trans_apply,
lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm, LinearEquiv.refl_apply,
rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply, lTensorHomToHomLTensor_apply,
rTensorHomToHomRTensor_apply, homTensorHomMap_apply, map_tmul]
