restrictScalarsLI — Mathlib

English

Norms are preserved under restrictScalars for continuous alternating maps.

Русский

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

LaTeX

$$$\|f\!\restrictionScalars 𝕜'\| = \|f\|$$$

Lean4

/-- `ContinuousAlternatingMap.restrictScalars` as a `LinearIsometry`. -/
@[simps]
def restrictScalarsLI : E [⋀^ι]→L[𝕜] F →ₗᵢ[𝕜'] E [⋀^ι]→L[𝕜'] F
    where
  toFun := restrictScalars 𝕜'
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  norm_map' _ := rfl

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