ringQuot_ext — Mathlib

English

Let f,g be RingHomorphisms from RingQuot r to T. If f ∘ mkRingHom r = g ∘ mkRingHom r, then f = g.

Русский

Пусть f,g — кольцевые однородности из RingQuot r в T. Если f ∘ mkRingHom r = g ∘ mkRingHom r, тогда f = g.

LaTeX

$$$\\forall f,g:\\, RingQuot r \\to\\!+* T,\\ (f \\circ mkRingHom r) = (g \\circ mkRingHom r)\\Rightarrow f = g$$$

Lean4

@[ext 1100]
theorem ringQuot_ext [NonAssocSemiring T] {r : R → R → Prop} (f g : RingQuot r →+* T)
    (w : f.comp (mkRingHom r) = g.comp (mkRingHom r)) : f = g :=
  by
  ext x
  rcases mkRingHom_surjective r x with ⟨x, rfl⟩
  exact (RingHom.congr_fun w x :)

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