mathlib documentation

data.polynomial.monomial

Univariate monomials #

Preparatory lemmas for degree_basic.

@[instance]
def polynomial.infinite {R : Type u} [semiring R] [nontrivial R] :
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.ring_hom_ext {R : Type u} [semiring R] {S : Type u_1} [semiring S] {f g : polynomial R →+* S} (h₁ : ∀ (a : R), f (polynomial.C a) = g (polynomial.C a)) (h₂ : f polynomial.X = g polynomial.X) :
f = g
@[ext]
theorem polynomial.ring_hom_ext' {R : Type u} [semiring R] {S : Type u_1} [semiring S] {f g : polynomial R →+* S} (h₁ : f.comp polynomial.C = g.comp polynomial.C) (h₂ : f polynomial.X = g polynomial.X) :
f = g