instFunLike — Mathlib

English

The map sending a semilinear isometry to its underlying linear map is injective.

Русский

Отображение полилинейной изометрии к её базовому линейному отображению инъективно.

LaTeX

$$$\operatorname{toLinearMap}: (E \to_{\mathrm{semilinear}} E_2) \to (E\to E_2)$ is injective$$

Lean4

instance instFunLike : FunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂
    where
  coe f := f.toFun
  coe_injective' _ _ h := toLinearMap_injective (DFunLike.coe_injective h)

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