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

• @Polynomial.infinite = @Polynomial.infinite.proof_1

theorem Polynomial.card_support_le_one_iff_monomial {R : Type u} [Semiring R] {f : Polynomial R} : Finset.card (Polynomial.support f) ≤ 1 ↔ ∃ n a, 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