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 : p.Monic) : p = Polynomial.X ^ p.natDegree + ∑ i ∈ Finset.range p.natDegree, Polynomial.C (p.coeff i) * Polynomial.X ^ i

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Polynomial.Monic.comp_X_add_C {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (Polynomial.X + Polynomial.C r)).Monic

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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 : p.Monic) (map_eq : Polynomial.map f p = 1) : p = 1

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

@[simp]

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

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

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

theorem Polynomial.eq_of_monic_of_associated {R : Type u} [Semiring R] {p q : Polynomial R} (hp : p.Monic) (hq : q.Monic) (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, (f i).Monic) : (Multiset.map f t).prod.Monic

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

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

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

theorem Polynomial.irreducible_of_monic {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1

theorem Polynomial.Monic.irreducible_iff_natDegree {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0

theorem Polynomial.Monic.irreducible_iff_natDegree' {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Finset.Ioc 0 (p.natDegree / 2)

theorem Polynomial.Monic.irreducible_iff_lt_natDegree_lt {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ (q : Polynomial R), q.Monic → q.natDegree ∈ Finset.Ioc 0 (p.natDegree / 2) → ¬q ∣ p

Alternate phrasing of Polynomial.Monic.irreducible_iff_natDegree' where we only have to check one divisor at a time.

theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff {R : Type u} [CommSemiring R] [NoZeroDivisors R] {p : Polynomial R} (hm : p.Monic) (hnd : p.natDegree = 2) : ¬Irreducible p ↔ ∃ (c₁ : R) (c₂ : R), p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂

@[simp]

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

@[simp]

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

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.map f p).degree = p.degree

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.map f p).natDegree = p.natDegree

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.map f p).leadingCoeff = f p.leadingCoeff

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.map f p).nextCoeff = f p.nextCoeff

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.map f p).leadingCoeff = f p.leadingCoeff

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.map f p).Monic) : p.Monic

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} : p.Monic ↔ (Polynomial.map f p).Monic

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

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

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

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.comp_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} (hp : p.Monic) (r : R) : (p.comp (Polynomial.X - Polynomial.C r)).Monic

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

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

@[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 : p.Monic) {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 : p.Monic) {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 : p.Monic) {q : Polynomial R} : (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0

theorem Polynomial.Monic.mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : p.Monic) {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 : p.Monic) {q : Polynomial R} : q * p = 0 ↔ q = 0

theorem Polynomial.Monic.isRegular {R : Type u_1} [Ring R] {p : Polynomial R} (hp : p.Monic) : 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) : (k • p).degree = p.degree

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) : (k • p).natDegree = p.natDegree

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) : (k • p).leadingCoeff = k • p.leadingCoeff

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

theorem Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff {R : Type u} [Semiring R] {p : Polynomial R} (h : IsUnit p.leadingCoeff) {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 p.leadingCoeff) {q : Polynomial R} : q * p = 0 ↔ q = 0