lift_tmul — Mathlib

English

Heterobasic version of TensorProduct.lcurry: converts a tensor-map into a bilinear map by currying.

Русский

Гетеробазовая версия TensorProduct.lcurry: перевод отображения из тензора в би- линейное отображение путём каррирования.

LaTeX

$$$\text{lcurry} : (M \otimes_R N \to_A P) \to_B M \to_A N \to_R P$, с $\text{toFun} = \text{curry}$$$

Lean4

@[simp]
theorem lift_tmul (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : lift f (x ⊗ₜ y) = f x y :=
  rfl

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