Univariate monomials
Preparatory lemmas for degree_basic.
C a is the constant polynomial a.
C is provided as a ring homomorphism.
Equations
@[simp]
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.nonzero.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
theorem
polynomial.C_inj
{R : Type u}
{a b : R}
[semiring R] :
⇑polynomial.C a = ⇑polynomial.C b ↔ a = b