coe_injective — Mathlib

English

COE map from semilinear maps to functions is injective: if their function parts are equal, the maps are equal.

Русский

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

LaTeX

$$$\text{Injective}(\mathrm{DFunLike.coe})$$$

Lean4

theorem coe_injective : Injective (DFunLike.coe : (M →ₛₗ[σ] M₃) → _) :=
  DFunLike.coe_injective

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