mathlib documentation

data.polynomial.monomial

Univariate monomials #

Preparatory lemmas for degree_basic.

source
def polynomial.C {R : Type u} [semiring R] :
R →+* polynomial R

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

Equations
source
@[simp]
theorem polynomial.monomial_zero_left {R : Type u} [semiring R] (a : R) :
⇑(polynomial.monomial 0) a = ⇑polynomial.C a
source
theorem polynomial.C_0 {R : Type u} [semiring R] :
⇑polynomial.C 0 = 0
source
theorem polynomial.C_1 {R : Type u} [semiring R] :
⇑polynomial.C 1 = 1
source
theorem polynomial.C_mul {R : Type u} {a b : R} [semiring R] :
⇑polynomial.C (a * b) = (⇑polynomial.C a) * ⇑polynomial.C b
source
theorem polynomial.C_add {R : Type u} {a b : R} [semiring R] :
⇑polynomial.C (a + b) = ⇑polynomial.C a + ⇑polynomial.C b
source
@[simp]
theorem polynomial.C_bit0 {R : Type u} {a : R} [semiring R] :
⇑polynomial.C (bit0 a) = bit0 (⇑polynomial.C a)
source
@[simp]
theorem polynomial.C_bit1 {R : Type u} {a : R} [semiring R] :
⇑polynomial.C (bit1 a) = bit1 (⇑polynomial.C a)
source
theorem polynomial.C_pow {R : Type u} {a : R} {n : ℕ} [semiring R] :
⇑polynomial.C (a ^ n) = ⇑polynomial.C a ^ n
source
@[simp]
theorem polynomial.C_mul_monomial {R : Type u} {a b : R} {n : ℕ} [semiring R] :
(⇑polynomial.C a) * ⇑(polynomial.monomial n) b = ⇑(polynomial.monomial n) (a * b)
source
@[simp]
theorem polynomial.monomial_mul_C {R : Type u} {a b : R} {n : ℕ} [semiring R] :
(⇑(polynomial.monomial n) a) * ⇑polynomial.C b = ⇑(polynomial.monomial n) (a * b)
source
@[simp]
theorem polynomial.C_eq_nat_cast {R : Type u} [semiring R] (n : ℕ) :
⇑polynomial.C ↑n = ↑n
source
@[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) :
finsupp.sum (⇑polynomial.C a) f = f 0 a
source
theorem polynomial.coeff_C {R : Type u} {a : R} {n : ℕ} [semiring R] :
(⇑polynomial.C a).coeff n = ite (n = 0) a 0
source
@[simp]
theorem polynomial.coeff_C_zero {R : Type u} {a : R} [semiring R] :
(⇑polynomial.C a).coeff 0 = a
source
theorem polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [semiring R] (h : n ≠ 0) :
(⇑polynomial.C a).coeff n = 0
source
theorem polynomial.nontrivial.of_polynomial_ne {R : Type u} [semiring R] {p q : polynomial R} (h : p ≠ q) :
nontrivial R
source
theorem polynomial.single_eq_C_mul_X {R : Type u} {a : R} [semiring R] {n : ℕ} :
⇑(polynomial.monomial n) a = (⇑polynomial.C a) * polynomial.X ^ n
source
@[simp]
theorem polynomial.C_inj {R : Type u} {a b : R} [semiring R] :
⇑polynomial.C a = ⇑polynomial.C b ↔ a = b
source
@[simp]
theorem polynomial.C_eq_zero {R : Type u} {a : R} [semiring R] :
⇑polynomial.C a = 0 ↔ a = 0
source
@[instance]
def polynomial.infinite {R : Type u} [semiring R] [nontrivial R] :
infinite (polynomial R)
source
theorem polynomial.monomial_eq_smul_X {R : Type u} {a : R} [semiring R] {n : ℕ} :
⇑(polynomial.monomial n) a = a • polynomial.X ^ n
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