curry — Mathlib

English

For a ∈ A and x ∈ M ⊗_R N, a • x equals (lsmul a) tensored with x on N.

Русский

Для a ∈ A и x ∈ M ⊗_R N, a • x равно (lsmul a) ⊗ x на N.

LaTeX

$$a \cdot x = (lsmul(R,R,M,a)).rTensor N x$$

Lean4

/-- Heterobasic version of `TensorProduct.curry`:

Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical
bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`. -/
@[simps]
nonrec def curry (f : M ⊗[R] N →ₗ[A] P) : M →ₗ[A] N →ₗ[R] P :=
  { curry (f.restrictScalars R) with
    toFun := curry (f.restrictScalars R)
    map_smul' := fun c x => LinearMap.ext fun y => f.map_smul c (x ⊗ₜ y) }

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