mathlib3 documentation

data.polynomial.monomial

Univariate monomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Preparatory lemmas for degree_basic.

source
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
source
@[protected, instance]
def polynomial.infinite {R : Type u} [semiring R] [nontrivial R] :
infinite (polynomial R)
source
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
source
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
source
@[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