Documentation

Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

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.

structure Polynomial.IsMonicOfDegree {R : Type u_1} [Semiring R] (p : Polynomial R) (n : ) :

This says that p has natDegree n and is monic.

Instances For
    theorem Polynomial.IsMonicOfDegree.exists_natDegree_lt {R : Type u_1} [Semiring R] {p : Polynomial R} {n : } (hn : n 0) (hp : p.IsMonicOfDegree n) :
    ∃ (q : Polynomial R), p = X ^ n + q q.natDegree < 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) :
    p.coeff m = q.coeff 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)) :
    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)) :
    theorem Polynomial.IsMonicOfDegree.add_right {R : Type u_1} [Semiring R] {p q : Polynomial R} {n : } (hp : p.IsMonicOfDegree n) (hq : q.natDegree < 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) :
    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) :
    p 0
    theorem Polynomial.isMonicOfDegree_one_iff {R : Type u_1} [Semiring R] [Nontrivial R] {f : Polynomial R} :
    f.IsMonicOfDegree 1 ∃ (r : R), f = X + C r
    theorem Polynomial.isMonicOfDegree_two_iff {R : Type u_1} [Semiring R] [Nontrivial R] {f : Polynomial R} :
    f.IsMonicOfDegree 2 ∃ (a : R) (b : R), f = X ^ 2 + C a * X + C b
    theorem Polynomial.IsMonicOfDegree.natDegree_sub_X_pow {R : Type u_1} [Ring R] {p : Polynomial R} {n : } (hn : n 0) (hp : p.IsMonicOfDegree n) :
    (p - X ^ n).natDegree < 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) :
    (p - q).natDegree < n
    theorem Polynomial.IsMonicOfDegree.sub {R : Type u_1} [Ring R] {p q : Polynomial R} {n : } (hp : p.IsMonicOfDegree n) (hq : q.natDegree < n) :
    theorem Polynomial.isMonicOfDegree_sub_add_two {R : Type u_1} [Ring R] [Nontrivial R] (a b : R) :
    (X ^ 2 - C a * X + C b).IsMonicOfDegree 2
    theorem Polynomial.isMonicOfDegree_two_iff' {R : Type u_1} [Ring R] [Nontrivial R] {f : Polynomial R} :
    f.IsMonicOfDegree 2 ∃ (a : R) (b : R), f = X ^ 2 - C a * X + C b

    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