hom_eq_hom — Mathlib

English

If two ring homomorphisms from MvPolynomial σ R to S₂ agree on all constants and on all X_i, then they are equal.

Русский

Если два кольцевых гомоморфизма из MvPolynomial σ R в S₂ совпадают на всех константах и на всех X_i, то они равны.

LaTeX

$$$\\\\forall f,g: RingHom (MvPolynomial\\\\sigma\\\\,R) S₂, \\\\Big( f ∘ MvPolynomial.C = g ∘ MvPolynomial.C \\\\Big) \\\\land \\\\Big( \\\\forall i, f(X i) = g(X i) \\\\Big) \\\\Rightarrow f = g$$$

Lean4

theorem hom_eq_hom [Semiring S₂] (f g : MvPolynomial σ R →+* S₂) (hC : f.comp C = g.comp C)
    (hX : ∀ n : σ, f (X n) = g (X n)) (p : MvPolynomial σ R) : f p = g p :=
  RingHom.congr_fun (ringHom_ext' hC hX) p

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