instSemilinearIsometryClass — Mathlib

English

Provide the structure making semilinear isometries into a SemilinearIsometryClass by defining map_add, map_smul, and norm_map.

Русский

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

LaTeX

$$$\text{instance }\text{SemilinearIsometryClass}$ with map_add, map_smulₛₗ, norm_map$$

Lean4

instance instSemilinearIsometryClass : SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
    where
  map_add f := map_add f.toLinearMap
  map_smulₛₗ f := map_smulₛₗ f.toLinearMap
  norm_map f := f.norm_map'

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