bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp

English

Restricting scalars in a bilinear map 𝕜' yields the same as composing the appropriate scalar-restriction maps: bilinearRestrictScalars 𝕜 B = (restrictScalarsL 𝕜' F G 𝕜 𝕜).comp (B.restrictScalars 𝕜).

Русский

Ограничение скаляров в билинейном отображении 𝕜' равно композиции соответствующих отображений ограничения скаляров.

LaTeX

$$$ B.bilinearRestrictScalars 𝕜 = \\big(\\text{restrictScalarsL } 𝕜' F G 𝕜 𝕜\\big) \\circ B.restrictScalars 𝕜 $$$

Lean4

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

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