Polynomial.ringHom_ext'

theorem Polynomial.ringHom_ext' : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : Semiring S] {f g : Polynomial R →+* S}, f.comp Polynomial.C = g.comp Polynomial.C → f Polynomial.X = g Polynomial.X → f = g

The theorem `Polynomial.ringHom_ext'` states that for any two ring homomorphisms `f` and `g` from the ring of polynomials over a semiring `R` into another semiring `S`, if these two ring homomorphisms agree on constant polynomials and on the polynomial indeterminate `X`, then the two ring homomorphisms are actually the same. In other words, a ring homomorphism on the polynomial ring is uniquely determined by its values on constants and on the polynomial indeterminate `X`.

More concisely: If two ring homomorphisms from the polynomial ring over a semiring agree on constants and the polynomial indeterminate, then they are equal.