ringHom_ext — Mathlib

English

Two ring homomorphisms from the direct sum are equal if they agree on the images of every generator coming from A_i.

Русский

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

LaTeX

$$$$\\text{Let }f,g:(\\bigoplus_i A_i)\\to R\\text{ be ring homomorphisms. If }\\forall i,x,\\ f(\\operatorname{of} A_i x)=g(\\operatorname{of} A_i x),\\text{ then }f=g.$$$$

Lean4

/-- Two `RingHom`s out of a direct sum are equal if they agree on the generators. -/
theorem ringHom_ext ⦃f g : (⨁ i, A i) →+* R⦄ (h : ∀ i x, f (of A i x) = g (of A i x)) : f = g :=
  ringHom_ext' fun i => AddMonoidHom.ext <| h i

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