Univariate monomials

Preparatory lemmas for degree_basic.

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

instance Polynomial.infinite {R : Type u} [Semiring R] [Nontrivial R] : Infinite (Polynomial R)

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