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_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 → β} :
f 0 0 = 0finsupp.sum (polynomial.C a) f = f 0 a

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.nontrivial.of_polynomial_ne {R : Type u} [semiring R] {p q : polynomial R} :
p qnontrivial R

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} :
(∀ (a : R), f (polynomial.C a) = g (polynomial.C a))f polynomial.X = g polynomial.Xf = g

@[ext]
theorem polynomial.ring_hom_ext' {R : Type u} [semiring R] {S : Type u_1} [semiring S] {f g : polynomial R →+* S} :