restrictScalarsRange₂ — Mathlib

English

There is a bilinear map restrictScalarsRange₂ : M' × N' → P' obtained by restricting scalars, domains, and range; it satisfies k (restrictScalarsRange₂ i j k hk B hB m n) = B(i m)(j n).

Русский

Существует билинейное отображение restrictScalarsRange₂: M' × N' → P', получаемое ограничением скаляр, доменов и диапазона; выполняется k(restrictScalarsRange₂ i j k hk B hB m n) = B(i m)(j n).

LaTeX

$$$k\big(\,restrictScalarsRange_2\ i\ j\ k\ hk\ B\ hB\ m\ n\big) = B(i m)(j n).$$$

Lean4

/-- Restrict the scalars, domains, and range of a bilinear map. -/
noncomputable def restrictScalarsRange₂ : M' →ₗ[S] N' →ₗ[S] P' :=
  (((LinearMap.restrictScalarsₗ S R _ _ _).comp (B.restrictScalars S)).compl₁₂ i j).codRestrict₂ k hk hB

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