ringHom_ext — Mathlib

English

Two ring homomorphisms from a quotient are equal if they agree on all cosets.

Русский

Два кольцевых гомоморфизма из факторкольца равны, если они совпадают на всех косетах.

LaTeX

$$$f,g: R/I \\to S,\\ f\\circ \\pi_I = g\\circ \\pi_I \\Rightarrow f=g$$$

Lean4

/-- Two `RingHom`s from the quotient by an ideal are equal if their
compositions with `Ideal.Quotient.mk'` are equal.

See note [partially-applied ext lemmas]. -/
@[ext 1100]
theorem ringHom_ext [NonAssocSemiring S] ⦃f g : R ⧸ I →+* S⦄ (h : f.comp (mk I) = g.comp (mk I)) : f = g :=
  RingHom.ext fun x => Quotient.inductionOn' x <| (RingHom.congr_fun h :)

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