Univariate monomials
Preparatory lemmas for degree_basic.
C a is the constant polynomial a.
C is provided as a ring homomorphism.
@[simp]
theorem
polynomial.monomial_zero_left
{R : Type u}
[semiring R]
(a : R) :
⇑(polynomial.monomial 0) a = ⇑polynomial.C a
theorem
polynomial.C_mul
{R : Type u}
{a b : R}
[semiring R] :
⇑polynomial.C (a * b) = (⇑polynomial.C a) * ⇑polynomial.C b
theorem
polynomial.C_add
{R : Type u}
{a b : R}
[semiring R] :
⇑polynomial.C (a + b) = ⇑polynomial.C a + ⇑polynomial.C b
@[simp]
theorem
polynomial.C_bit0
{R : Type u}
{a : R}
[semiring R] :
⇑polynomial.C (bit0 a) = bit0 (⇑polynomial.C a)
@[simp]
theorem
polynomial.C_bit1
{R : Type u}
{a : R}
[semiring R] :
⇑polynomial.C (bit1 a) = bit1 (⇑polynomial.C a)
theorem
polynomial.C_pow
{R : Type u}
{a : R}
{n : ℕ}
[semiring R] :
⇑polynomial.C (a ^ n) = ⇑polynomial.C a ^ n
@[simp]
@[simp]
theorem
polynomial.sum_C_index
{R : Type u}
[semiring R]
{a : R}
{β : Type u_1}
[add_comm_monoid β]
{f : ℕ → R → β} :
f 0 0 = 0 → finsupp.sum (⇑polynomial.C a) f = f 0 a
@[simp]
theorem
polynomial.nontrivial.of_polynomial_ne
{R : Type u}
[semiring R]
{p q : polynomial R} :
p ≠ q → nontrivial R
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
@[simp]
theorem
polynomial.C_inj
{R : Type u}
{a b : R}
[semiring R] :
⇑polynomial.C a = ⇑polynomial.C b ↔ a = b
@[simp]
@[instance]
theorem
polynomial.monomial_eq_smul_X
{R : Type u}
{a : R}
[semiring R]
{n : ℕ} :
⇑(polynomial.monomial n) a = a • polynomial.X ^ 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.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} :
f.comp polynomial.C = g.comp polynomial.C → ⇑f polynomial.X = ⇑g polynomial.X → f = g