coe_restrictScalarsIsometry — Mathlib

English

There is a canonical isometry between scalar-restricted map spaces, and its underlying linear map equals the standard restriction map.

Русский

Существует каноническая изометрия между пространствами отображений с ограничением скаляров, чья сопряженная линейная карта равна обычному ограничению скаляров.

LaTeX

$$$ \\text{coe\_restrictScalarsIsometry} = \\text{restrictScalars} $$$

Lean4

@[simp]
theorem coe_restrictScalarsIsometry : ⇑(restrictScalarsIsometry 𝕜 E Fₗ 𝕜' 𝕜'') = restrictScalars 𝕜' :=
  rfl

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