Theory of monic polynomials

We give several tools for proving that polynomials are monic, e.g. Monic.mul, Monic.map, Monic.pow.

theorem Polynomial.monic_zero_iff_subsingleton {R : Type u} [Semiring R] : Polynomial.Monic 0 ↔ Subsingleton R

theorem Polynomial.not_monic_zero_iff {R : Type u} [Semiring R] : ¬Polynomial.Monic 0 ↔ 0 ≠ 1

theorem Polynomial.monic_zero_iff_subsingleton' {R : Type u} [Semiring R] : Polynomial.Monic 0 ↔ (∀ (f g : Polynomial R), f = g) ∧ ∀ (a b : R), a = b

theorem Polynomial.Monic.as_sum {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) : p = Polynomial.X ^ Polynomial.natDegree p + Finset.sum (Finset.range (Polynomial.natDegree p)) fun (i : ℕ) => Polynomial.C (Polynomial.coeff p i) * Polynomial.X ^ i

theorem Polynomial.ne_zero_of_ne_zero_of_monic {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : p ≠ 0) (hq : Polynomial.Monic q) : q ≠ 0

theorem Polynomial.Monic.map {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (hp : Polynomial.Monic p) : Polynomial.Monic (Polynomial.map f p)

theorem Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : b * Polynomial.leadingCoeff p = 1) : Polynomial.Monic (Polynomial.C b * p)

theorem Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {b : R} (hp : Polynomial.leadingCoeff p * b = 1) : Polynomial.Monic (p * Polynomial.C b)

theorem Polynomial.monic_of_degree_le {R : Type u} [Semiring R] {p : Polynomial R} (n : ℕ) (H1 : Polynomial.degree p ≤ ↑n) (H2 : Polynomial.coeff p n = 1) : Polynomial.Monic p

theorem Polynomial.monic_X_pow_add {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (H : Polynomial.degree p ≤ ↑n) : Polynomial.Monic (Polynomial.X ^ (n + 1) + p)

theorem Polynomial.monic_X_pow_add_C {R : Type u} (a : R) [Semiring R] {n : ℕ} (h : n ≠ 0) : Polynomial.Monic (Polynomial.X ^ n + Polynomial.C a)

theorem Polynomial.monic_X_add_C {R : Type u} [Semiring R] (x : R) : Polynomial.Monic (Polynomial.X + Polynomial.C x)

theorem Polynomial.Monic.mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) : Polynomial.Monic (p * q)

theorem Polynomial.Monic.pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) (n : ℕ) : Polynomial.Monic (p ^ n)

theorem Polynomial.Monic.add_of_left {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hpq : Polynomial.degree q < Polynomial.degree p) : Polynomial.Monic (p + q)

theorem Polynomial.Monic.add_of_right {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) (hpq : Polynomial.degree p < Polynomial.degree q) : Polynomial.Monic (p + q)

theorem Polynomial.Monic.of_mul_monic_left {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hpq : Polynomial.Monic (p * q)) : Polynomial.Monic q

theorem Polynomial.Monic.of_mul_monic_right {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.Monic q) (hpq : Polynomial.Monic (p * q)) : Polynomial.Monic p

@[simp]

theorem Polynomial.Monic.natDegree_eq_zero_iff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) : Polynomial.natDegree p = 0 ↔ p = 1

@[simp]

theorem Polynomial.Monic.degree_le_zero_iff_eq_one {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) : Polynomial.degree p ≤ 0 ↔ p = 1

theorem Polynomial.Monic.natDegree_mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) : Polynomial.natDegree (p * q) = Polynomial.natDegree p + Polynomial.natDegree q

theorem Polynomial.Monic.degree_mul_comm {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) (q : Polynomial R) : Polynomial.degree (p * q) = Polynomial.degree (q * p)

theorem Polynomial.Monic.natDegree_mul' {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : q ≠ 0) : Polynomial.natDegree (p * q) = Polynomial.natDegree p + Polynomial.natDegree q

theorem Polynomial.Monic.natDegree_mul_comm {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) (q : Polynomial R) : Polynomial.natDegree (p * q) = Polynomial.natDegree (q * p)

theorem Polynomial.Monic.not_dvd_of_natDegree_lt {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (h0 : q ≠ 0) (hl : Polynomial.natDegree q < Polynomial.natDegree p) : ¬p ∣ q

theorem Polynomial.Monic.not_dvd_of_degree_lt {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (h0 : q ≠ 0) (hl : Polynomial.degree q < Polynomial.degree p) : ¬p ∣ q

theorem Polynomial.Monic.nextCoeff_mul {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) : Polynomial.nextCoeff (p * q) = Polynomial.nextCoeff p + Polynomial.nextCoeff q

theorem Polynomial.Monic.nextCoeff_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) (n : ℕ) : Polynomial.nextCoeff (p ^ n) = n • Polynomial.nextCoeff p

theorem Polynomial.Monic.eq_one_of_map_eq_one {R : Type u} [Semiring R] {p : Polynomial R} {S : Type u_1} [Semiring S] [Nontrivial S] (f : R →+* S) (hp : Polynomial.Monic p) (map_eq : Polynomial.map f p = 1) : p = 1

theorem Polynomial.Monic.natDegree_pow {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) (n : ℕ) : Polynomial.natDegree (p ^ n) = n * Polynomial.natDegree p

@[simp]

theorem Polynomial.natDegree_pow_X_add_C {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) (r : R) : Polynomial.natDegree ((Polynomial.X + Polynomial.C r) ^ n) = n

theorem Polynomial.Monic.eq_one_of_isUnit {R : Type u} [Semiring R] {p : Polynomial R} (hm : Polynomial.Monic p) (hpu : IsUnit p) : p = 1

theorem Polynomial.Monic.isUnit_iff {R : Type u} [Semiring R] {p : Polynomial R} (hm : Polynomial.Monic p) : IsUnit p ↔ p = 1

theorem Polynomial.eq_of_monic_of_associated {R : Type u} [Semiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hq : Polynomial.Monic q) (hpq : Associated p q) : p = q

theorem Polynomial.monic_multiset_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R) (ht : ∀ i ∈ t, Polynomial.Monic (f i)) : Polynomial.Monic (Multiset.prod (Multiset.map f t))

theorem Polynomial.monic_prod_of_monic {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (hs : ∀ i ∈ s, Polynomial.Monic (f i)) : Polynomial.Monic (Finset.prod s fun (i : ι) => f i)

theorem Polynomial.Monic.nextCoeff_multiset_prod {R : Type u} {ι : Type y} [CommSemiring R] (t : Multiset ι) (f : ι → Polynomial R) (h : ∀ i ∈ t, Polynomial.Monic (f i)) : Polynomial.nextCoeff (Multiset.prod (Multiset.map f t)) = Multiset.sum (Multiset.map (fun (i : ι) => Polynomial.nextCoeff (f i)) t)

theorem Polynomial.Monic.nextCoeff_prod {R : Type u} {ι : Type y} [CommSemiring R] (s : Finset ι) (f : ι → Polynomial R) (h : ∀ i ∈ s, Polynomial.Monic (f i)) : Polynomial.nextCoeff (Finset.prod s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Polynomial.nextCoeff (f i)

@[simp]

theorem Polynomial.Monic.natDegree_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : Polynomial.Monic P) (f : R →+* S) : Polynomial.natDegree (Polynomial.map f P) = Polynomial.natDegree P

@[simp]

theorem Polynomial.Monic.degree_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] [Nontrivial S] {P : Polynomial R} (hmo : Polynomial.Monic P) (f : R →+* S) : Polynomial.degree (Polynomial.map f P) = Polynomial.degree P

theorem Polynomial.degree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : Polynomial.degree (Polynomial.map f p) = Polynomial.degree p

theorem Polynomial.natDegree_map_eq_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : Polynomial.natDegree (Polynomial.map f p) = Polynomial.natDegree p

theorem Polynomial.leadingCoeff_map' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : Polynomial.leadingCoeff (Polynomial.map f p) = f (Polynomial.leadingCoeff p)

theorem Polynomial.nextCoeff_map {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : Polynomial.nextCoeff (Polynomial.map f p) = f (Polynomial.nextCoeff p)

theorem Polynomial.leadingCoeff_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) (p : Polynomial R) : Polynomial.leadingCoeff (Polynomial.map f p) = f (Polynomial.leadingCoeff p)

theorem Polynomial.monic_of_injective {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {p : Polynomial R} (hp : Polynomial.Monic (Polynomial.map f p)) : Polynomial.Monic p

theorem Function.Injective.monic_map_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {p : Polynomial R} : Polynomial.Monic p ↔ Polynomial.Monic (Polynomial.map f p)

theorem Polynomial.monic_X_sub_C {R : Type u} [Ring R] (x : R) : Polynomial.Monic (Polynomial.X - Polynomial.C x)

theorem Polynomial.monic_X_pow_sub {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} (H : Polynomial.degree p ≤ ↑n) : Polynomial.Monic (Polynomial.X ^ (n + 1) - p)

theorem Polynomial.monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : Polynomial.Monic (Polynomial.X ^ n - Polynomial.C a)

X ^ n - a is monic.

theorem Polynomial.not_isUnit_X_pow_sub_one (R : Type u_1) [CommRing R] [Nontrivial R] (n : ℕ) : ¬IsUnit (Polynomial.X ^ n - 1)

theorem Polynomial.Monic.sub_of_left {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Monic p) (hpq : Polynomial.degree q < Polynomial.degree p) : Polynomial.Monic (p - q)

theorem Polynomial.Monic.sub_of_right {R : Type u} [Ring R] {p : Polynomial R} {q : Polynomial R} (hq : Polynomial.leadingCoeff q = -1) (hpq : Polynomial.degree p < Polynomial.degree q) : Polynomial.Monic (p - q)

@[simp]

theorem Polynomial.not_monic_zero {R : Type u} [Semiring R] [Nontrivial R] : ¬Polynomial.Monic 0

theorem Polynomial.Monic.mul_left_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) {q : Polynomial R} (hq : q ≠ 0) : q * p ≠ 0

theorem Polynomial.Monic.mul_right_ne_zero {R : Type u} [Semiring R] {p : Polynomial R} (hp : Polynomial.Monic p) {q : Polynomial R} (hq : q ≠ 0) : p * q ≠ 0

theorem Polynomial.Monic.mul_natDegree_lt_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.Monic p) {q : Polynomial R} : Polynomial.natDegree (p * q) < Polynomial.natDegree p ↔ p ≠ 1 ∧ q = 0

theorem Polynomial.Monic.mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.Monic p) {q : Polynomial R} : p * q = 0 ↔ q = 0

theorem Polynomial.Monic.mul_left_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : Polynomial.Monic p) {q : Polynomial R} : q * p = 0 ↔ q = 0

theorem Polynomial.Monic.isRegular {R : Type u_1} [Ring R] {p : Polynomial R} (hp : Polynomial.Monic p) : IsRegular p

theorem Polynomial.degree_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : Polynomial.degree (k • p) = Polynomial.degree p

theorem Polynomial.natDegree_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : Polynomial.natDegree (k • p) = Polynomial.natDegree p

theorem Polynomial.leadingCoeff_smul_of_smul_regular {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] {k : S} (p : Polynomial R) (h : IsSMulRegular R k) : Polynomial.leadingCoeff (k • p) = k • Polynomial.leadingCoeff p

theorem Polynomial.monic_of_isUnit_leadingCoeff_inv_smul {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit (Polynomial.leadingCoeff p)) : Polynomial.Monic ((IsUnit.unit h)⁻¹ • p)

theorem Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit (Polynomial.leadingCoeff p)) {q : Polynomial R} : p * q = 0 ↔ q = 0

theorem Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit (Polynomial.leadingCoeff p)) {q : Polynomial R} : q * p = 0 ↔ q = 0