Documentation

Mathlib.Data.Polynomial.Monomial

Univariate monomials #

Preparatory lemmas for degree_basic.

theorem Polynomial.ringHom_ext {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f : Polynomial R →+* S} {g : Polynomial R →+* S} (h₁ : ∀ (a : R), f (Polynomial.C a) = g (Polynomial.C a)) (h₂ : f Polynomial.X = g Polynomial.X) :
f = g
theorem Polynomial.ringHom_ext' {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f : Polynomial R →+* S} {g : Polynomial R →+* S} (h₁ : RingHom.comp f Polynomial.C = RingHom.comp g Polynomial.C) (h₂ : f Polynomial.X = g Polynomial.X) :
f = g