restrictScalars_curry — Mathlib

English

The operation of restricting scalars commutes with curry: restrictScalars R (curry f) equals curry of restrictScalars R f.

Русский

Ограничение скалярных умножений commute: restrictScalars R (curry f) = curry (restrictScalars R f).

LaTeX

$$restrictScalars R (curry f) = TensorProduct.curry (f.restrictScalars R)$$

Lean4

theorem restrictScalars_curry (f : M ⊗[R] N →ₗ[A] P) :
    restrictScalars R (curry f) = TensorProduct.curry (f.restrictScalars R) :=
  rfl

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