coe_monoidHom_injective — Mathlib

English

Let f,g be ring homomorphisms α →+* β. If they are equal as monoid homomorphisms (i.e., their multiplicative structures coincide), then f = g.

Русский

Пусть f,g: α →+* β — кольцевые гомоморфизмы. Если они совпадают как моноидные гомоморфизмы, то f = g.

LaTeX

$$$\forall f,g:\alpha \to+*\beta,\ (f : \alpha \to*\beta) = (g : \alpha \to*\beta) \rightarrow f = g$$$

Lean4

theorem coe_monoidHom_injective : Injective (fun f : α →+* β => (f : α →* β)) :=
  Injective.of_comp (f := DFunLike.coe) DFunLike.coe_injective

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