coe_ringHom_injective — Mathlib

English

The map that sends an AlgHom to its underlying RingHom is injective: if two AlgHoms have the same RingHom part, they are equal.

Русский

Отображение, отправляющее AlgHom в его RingHom-часть, инъективно: если две AlgHom имеют одинаковую RingHom-часть, то они равны.

LaTeX

$$\\n\$\\text{AlgHom}.coe\\_ringHom\\_injective\$ : (A \\to_ R B) \\to (A \\to^+* B) is injective$$

Lean4

theorem coe_ringHom_injective : Function.Injective ((↑) : (A →ₐ[R] B) → A →+* B) := fun φ₁ φ₂ H =>
  coe_fn_injective <| show ((φ₁ : A →+* B) : A → B) = ((φ₂ : A →+* B) : A → B) from congr_arg _ H

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