bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars

English

For B: E →L[𝕜'] F →L[𝕜'] G, the bilinear restriction equals applying B to its arguments: (B.bilinearRestrictScalars 𝕜) x y = B x y.

Русский

Для B: E →L[𝕜'] F →L[𝕜'] G вернем bilinearRestrictScalars 𝕜 и получим применение: (B.bilinearRestrictScalars 𝕜) x y = B x y.

LaTeX

$$$ (B.bilinearRestrictScalars 𝕜)\\,x\\,y = B\\,x\\,y $$$

Lean4

theorem bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars :
    B.bilinearRestrictScalars 𝕜 = (restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (B.restrictScalars 𝕜) :=
  rfl

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