Univariate monomials

Preparatory lemmas for degree_basic.

theorem Polynomial.monomial_one_eq_iff {R : Type u} [Semiring R] [Nontrivial R] {i j : ℕ} : (monomial i) 1 = (monomial j) 1 ↔ i = j

instance Polynomial.infinite {R : Type u} [Semiring R] [Nontrivial R] : Infinite (Polynomial 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 = (monomial n) a

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

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