instLinearEquivClass — Mathlib

English

There is a canonical coercion from isometric equivalences to linear equivalences: an isometry equivalence corresponds to a linear equivalence between the underlying modules.

Русский

Существует каноническое отображение изометрических эквивалентностей в линейные эквивалентности: изометрическая эквивалентность соответствует линейной эквививалентности между базовыми модулями.

LaTeX

$$$\text{IsometryEquiv} \to (M_1 \simeq_R M_2)$$$

Lean4

instance : LinearEquivClass (Q₁.IsometryEquiv Q₂) R M₁ M₂
    where
  map_add f := map_add f.toLinearEquiv
  map_smulₛₗ f := map_smulₛₗ f.toLinearEquiv

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