Documentation

Mathlib.Algebra.Polynomial.Monomial

Univariate monomials #

Preparatory lemmas for degree_basic.

Equations
  • =
theorem Polynomial.card_support_le_one_iff_monomial {R : Type u} [Semiring R] {f : Polynomial R} :
f.support.card 1 ∃ (n : ) (a : R), f = (Polynomial.monomial n) a
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'_iff {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f : Polynomial R →+* S} {g : Polynomial R →+* S} :
f = g f.comp Polynomial.C = g.comp Polynomial.C f Polynomial.X = g Polynomial.X
theorem Polynomial.ringHom_ext' {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] {f : Polynomial R →+* S} {g : Polynomial R →+* S} (h₁ : f.comp Polynomial.C = g.comp Polynomial.C) (h₂ : f Polynomial.X = g Polynomial.X) :
f = g