norm_restrictScalars — Mathlib

English

Restricting scalars along a scalar tower defines a linear isometry between spaces of alternating maps with different base fields.

Русский

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

LaTeX

$$$\text{restrictScalarsLI} : E [⋀^ι]→L[\mathbb{K}'] F \to E [⋀^ι]→L[\mathbb{K}] F$ is a linear isometry.$$

Lean4

@[simp]
theorem norm_restrictScalars : ‖f.restrictScalars 𝕜'‖ = ‖f‖ :=
  rfl

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