Monic polynomials of given degree #
This file defines the predicate Polynomial.IsMonicOfDegree p n
that states that
the polynomial p
is monic and has degree n
(i.e., p.natDegree = n
.)
We also provide some basic API.
@[simp]
theorem
Polynomial.IsMonicOfDegree.leadingCoeff_eq
{R : Type u_1}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
(hp : p.IsMonicOfDegree n)
:
@[simp]
theorem
Polynomial.isMonicOfDegree_iff_of_subsingleton
{R : Type u_1}
[Semiring R]
[Subsingleton R]
{p : Polynomial R}
{n : ℕ}
:
theorem
Polynomial.isMonicOfDegree_iff
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(p : Polynomial R)
(n : ℕ)
:
theorem
Polynomial.IsMonicOfDegree.exists_natDegree_lt
{R : Type u_1}
[Semiring R]
{p : Polynomial R}
{n : ℕ}
(hn : n ≠ 0)
(hp : p.IsMonicOfDegree n)
:
theorem
Polynomial.IsMonicOfDegree.mul
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{m n : ℕ}
(hp : p.IsMonicOfDegree m)
(hq : q.IsMonicOfDegree n)
:
(p * q).IsMonicOfDegree (m + n)
theorem
Polynomial.IsMonicOfDegree.pow
{R : Type u_1}
[Semiring R]
{p : Polynomial R}
{m : ℕ}
(hp : p.IsMonicOfDegree m)
(n : ℕ)
:
(p ^ n).IsMonicOfDegree (m * n)
theorem
Polynomial.IsMonicOfDegree.coeff_eq
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{n : ℕ}
(hp : p.IsMonicOfDegree n)
(hq : q.IsMonicOfDegree n)
{m : ℕ}
(hm : n ≤ m)
:
theorem
Polynomial.IsMonicOfDegree.of_mul_left
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{m n : ℕ}
(hp : p.IsMonicOfDegree m)
(hpq : (p * q).IsMonicOfDegree (m + n))
:
q.IsMonicOfDegree n
theorem
Polynomial.IsMonicOfDegree.of_mul_right
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{m n : ℕ}
(hq : q.IsMonicOfDegree n)
(hpq : (p * q).IsMonicOfDegree (m + n))
:
p.IsMonicOfDegree m
theorem
Polynomial.IsMonicOfDegree.add_right
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{n : ℕ}
(hp : p.IsMonicOfDegree n)
(hq : q.natDegree < n)
:
(p + q).IsMonicOfDegree n
theorem
Polynomial.IsMonicOfDegree.add_left
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{n : ℕ}
(hp : p.natDegree < n)
(hq : q.IsMonicOfDegree n)
:
(p + q).IsMonicOfDegree n
theorem
Polynomial.IsMonicOfDegree.comp
{R : Type u_1}
[Semiring R]
{p q : Polynomial R}
{m n : ℕ}
(hn : n ≠ 0)
(hp : p.IsMonicOfDegree m)
(hq : q.IsMonicOfDegree n)
:
(p.comp q).IsMonicOfDegree (m * n)
theorem
Polynomial.IsMonicOfDegree.ne_zero
{R : Type u_1}
[Semiring R]
[Nontrivial R]
{p : Polynomial R}
{n : ℕ}
(h : p.IsMonicOfDegree n)
:
theorem
Polynomial.isMonicOfDegree_X_pow
(R : Type u_1)
[Semiring R]
[Nontrivial R]
(n : ℕ)
:
(X ^ n).IsMonicOfDegree n
theorem
Polynomial.isMonicOfDegree_monomial_one
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(n : ℕ)
:
((monomial n) 1).IsMonicOfDegree n
theorem
Polynomial.isMonicOfDegree_X_add_one
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(r : R)
:
(X + C r).IsMonicOfDegree 1
theorem
Polynomial.isMonicOfDegree_one_iff
{R : Type u_1}
[Semiring R]
[Nontrivial R]
{f : Polynomial R}
:
theorem
Polynomial.isMonicOfDegree_add_add_two
{R : Type u_1}
[Semiring R]
[Nontrivial R]
(a b : R)
:
theorem
Polynomial.isMonicOfDegree_two_iff
{R : Type u_1}
[Semiring R]
[Nontrivial R]
{f : Polynomial R}
:
theorem
Polynomial.IsMonicOfDegree.natDegree_sub_X_pow
{R : Type u_1}
[Ring R]
{p : Polynomial R}
{n : ℕ}
(hn : n ≠ 0)
(hp : p.IsMonicOfDegree n)
:
theorem
Polynomial.IsMonicOfDegree.natDegree_sub_lt
{R : Type u_1}
[Ring R]
{p q : Polynomial R}
{n : ℕ}
(hn : n ≠ 0)
(hp : p.IsMonicOfDegree n)
(hq : q.IsMonicOfDegree n)
:
theorem
Polynomial.IsMonicOfDegree.sub
{R : Type u_1}
[Ring R]
{p q : Polynomial R}
{n : ℕ}
(hp : p.IsMonicOfDegree n)
(hq : q.natDegree < n)
:
(p - q).IsMonicOfDegree n
theorem
Polynomial.isMonicOfDegree_X_sub_one
{R : Type u_1}
[Ring R]
[Nontrivial R]
(r : R)
:
(X - C r).IsMonicOfDegree 1
theorem
Polynomial.isMonicOfDegree_two_iff'
{R : Type u_1}
[Ring R]
[Nontrivial R]
{f : Polynomial R}
:
A version of Polynomial.isMonicOfDegree_two_iff
with negated middle coefficient.
theorem
Polynomial.IsMonicOfDegree.of_dvd_add
{R : Type u_1}
[CommRing R]
{a b r : Polynomial R}
{m n : ℕ}
(hmn : n ≤ m)
(ha : a.IsMonicOfDegree m)
(hb : b.IsMonicOfDegree n)
(hr : r.natDegree < m)
(h : b ∣ a + r)
:
∃ (q : Polynomial R), q.IsMonicOfDegree (m - n) ∧ a = q * b - r
theorem
Polynomial.IsMonicOfDegree.of_dvd_sub
{R : Type u_1}
[CommRing R]
{a b r : Polynomial R}
{m n : ℕ}
(hmn : n ≤ m)
(ha : a.IsMonicOfDegree m)
(hb : b.IsMonicOfDegree n)
(hr : r.natDegree < m)
(h : b ∣ a - r)
:
∃ (q : Polynomial R), q.IsMonicOfDegree (m - n) ∧ a = q * b + r
theorem
Polynomial.IsMonicOfDegree.aeval_add
{R : Type u_1}
[CommRing R]
{p : Polynomial R}
{n : ℕ}
(hp : p.IsMonicOfDegree n)
(r : R)
:
((aeval (X + C r)) p).IsMonicOfDegree n
theorem
Polynomial.IsMonicOfDegree.aeval_sub
{R : Type u_1}
[CommRing R]
{p : Polynomial R}
{n : ℕ}
(hp : p.IsMonicOfDegree n)
(r : R)
:
((aeval (X - C r)) p).IsMonicOfDegree n