coe_algHom_injective — Mathlib

English

The coercion from algebra equivalences to algebra homomorphisms is injective; two algebra equivalences are equal if they induce the same algebra homomorphism.

Русский

Связь между алгебраическими эквивалентностями и их образами как алгебра-гомоморфизмов инъективна; равенство гомоморфизмов влечет равенство эквивалентностей.

LaTeX

$$$(e \mapsto e.toAlgHom)$ is injective;\quad e_1.toAlgHom = e_2.toAlgHom \Rightarrow e_1 = e_2$$$

Lean4

theorem coe_algHom_injective : Function.Injective ((↑) : (A₁ ≃ₐ[R] A₂) → A₁ →ₐ[R] A₂) := fun _ _ h =>
  ext <| AlgHom.congr_fun h

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