hom_ext — Mathlib

English

Let R and S be Boolean rings and f,g be morphisms from R to S in the category BoolRing. If the underlying ring homomorphisms are equal, then f and g are equal as BoolRing morphisms.

Русский

Пусть R и S — булевы кольца и f, g — морфизмы R → S в категории BoolRing. Если их соответствующие гомоморфизмы колец совпадают, то сами морфизмы равны.

LaTeX

$$$\\forall \\{R\\, S : BoolRing\\} \\{f\\, g : R \\to S\\}, f.hom = g.hom \\rightarrow f = g$$$

Lean4

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

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