hom_ext — Mathlib

English

If f,g: R ⟶ S are ring homomorphisms and they have the same underlying function (hf: f.hom = g.hom), then f = g.

Русский

Пусть f,g: R ⟶ S — гомоморфизмы колец, и их действие на элементы совпадает (f.hom = g.hom). Тогда f = g.

LaTeX

$$$ \forall R,S \; \forall f,g: R \to S,\ f.hom = g.hom \Rightarrow f = g. $$$$

Lean4

@[ext]
theorem hom_ext {R S : RingCat} {f g : R ⟶ S} (hf : f.hom = g.hom) : f = g :=
  Hom.ext hf

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