mathlib documentation

data.polynomial.monomial

Univariate monomials #

Preparatory lemmas for degree_basic.

def polynomial.C {R : Type u} [semiring R] :

C a is the constant polynomial a. C is provided as a ring homomorphism.

Equations
@[simp]
theorem polynomial.monomial_zero_left {R : Type u} [semiring R] (a : R) :
theorem polynomial.C_0 {R : Type u} [semiring R] :
theorem polynomial.C_1 {R : Type u} [semiring R] :
theorem polynomial.C_mul {R : Type u} {a b : R} [semiring R] :
theorem polynomial.C_add {R : Type u} {a b : R} [semiring R] :
@[simp]
theorem polynomial.C_bit0 {R : Type u} {a : R} [semiring R] :
@[simp]
theorem polynomial.C_bit1 {R : Type u} {a : R} [semiring R] :
theorem polynomial.C_pow {R : Type u} {a : R} {n : } [semiring R] :
@[simp]
theorem polynomial.C_mul_monomial {R : Type u} {a b : R} {n : } [semiring R] :
@[simp]
theorem polynomial.monomial_mul_C {R : Type u} {a b : R} {n : } [semiring R] :
@[simp]
theorem polynomial.C_eq_nat_cast {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.sum_C_index {R : Type u} [semiring R] {a : R} {β : Type u_1} [add_comm_monoid β] {f : R → β} (h : f 0 0 = 0) :
theorem polynomial.coeff_C {R : Type u} {a : R} {n : } [semiring R] :
(polynomial.C a).coeff n = ite (n = 0) a 0
@[simp]
theorem polynomial.coeff_C_zero {R : Type u} {a : R} [semiring R] :
theorem polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : } [semiring R] (h : n 0) :
theorem polynomial.nontrivial.of_polynomial_ne {R : Type u} [semiring R] {p q : polynomial R} (h : p q) :
theorem polynomial.single_eq_C_mul_X {R : Type u} {a : R} [semiring R] {n : } :
@[simp]
theorem polynomial.C_inj {R : Type u} {a b : R} [semiring R] :
@[simp]
theorem polynomial.C_eq_zero {R : Type u} {a : R} [semiring R] :
@[instance]
def polynomial.infinite {R : Type u} [semiring R] [nontrivial R] :
theorem polynomial.monomial_eq_smul_X {R : Type u} {a : R} [semiring R] {n : } :
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
@[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