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} : (Polynomial.support f).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' {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