English
The lift construction for IsTensorProduct is defined as the composition of TensorProduct.lift with the inverse equivalence; i.e., IsTensorProduct.lift h f' := (TensorProduct.lift f').comp h.equiv.symm.toLinearMap.
Русский
Конструкция подъёма для IsTensorProduct задаётся как композиция TensorProduct.lift и обратного эквив; IsTensorProduct.lift h f' := (TensorProduct.lift f').comp h.equiv.symm.toLinearMap.
LaTeX
$$IsTensorProduct.lift h f' = (TensorProduct.lift f').comp h.equiv.symm.toLinearMap$$
Lean4
/-- If `M` is the tensor product of `M₁` and `M₂`, we may lift a bilinear map `M₁ →ₗ[R] M₂ →ₗ[R] M'`
to a `M →ₗ[R] M'`. -/
noncomputable def lift (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') : M →ₗ[R] M' :=
(TensorProduct.lift f').comp h.equiv.symm.toLinearMap
