coe_injective — Mathlib

English

The coercion to functions from semilinear equivalences is injective: distinct semilinear equivalences have distinct underlying functions.

Русский

Коэрсионная отображение в функции от семилинейных эквивалентностей инъективно: разные эквивалентности дают разные функции.

LaTeX

$$Injective (LinearEquiv.coe) : @Injective (M ≃ₛₗ[σ] M₂) (M → M₂) (DFunLike.coe)$$

Lean4

theorem coe_injective : @Injective (M ≃ₛₗ[σ] M₂) (M → M₂) DFunLike.coe :=
  DFunLike.coe_injective

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