coe_injective — Mathlib

English

The underlying function map is injective: if two nonunital algebra homomorphisms have the same underlying function, they are equal.

Русский

Граф приведения к функции инъективен: если два гомоморфизма алгебры без единицы имеют одинаковую базовую функцию, они равны.

LaTeX

$$$\forall f,g : A \to_{\varphi} B,\ f.toFun = g.toFun \Rightarrow f = g$$$

Lean4

theorem coe_injective : @Function.Injective (A →ₛₙₐ[φ] B) (A → B) (↑) := by rintro ⟨⟨⟨f, _⟩, _⟩, _⟩ ⟨⟨⟨g, _⟩, _⟩, _⟩ h;
  congr

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