doc-next-gen

Mathlib.Algebra.Polynomial.Monic

Module docstring

{"# Theory of monic polynomials

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

Polynomial.not_monic_zero_iff theorem
: ¬Monic (0 : R[X]) ↔ (0 : R) ≠ 1
Full source 
theorem not_monic_zero_iff : ¬Monic (0 : R[X])¬Monic (0 : R[X]) ↔ (0 : R) ≠ 1 :=
  (monic_zero_iff_subsingleton.trans subsingleton_iff_zero_eq_one.symm).not
Non-Monicity of Zero Polynomial: $\neg \text{Monic}(0) \leftrightarrow 0 \neq 1$
Informal description
The zero polynomial $0 \in R[X]$ is not monic if and only if the zero element $0$ and the multiplicative identity $1$ in the semiring $R$ are distinct, i.e., $0 \neq 1$.
Polynomial.monic_zero_iff_subsingleton' theorem
: Monic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ ∀ a b : R, a = b
Full source 
theorem monic_zero_iff_subsingleton' :
    MonicMonic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ ∀ a b : R, a = b :=
  Polynomial.monic_zero_iff_subsingleton.trans
    ⟨by
      intro
      simp [eq_iff_true_of_subsingleton], fun h => subsingleton_iff.mpr h.2⟩
Monic Zero Polynomial Characterization: $\text{Monic}(0) \leftrightarrow (\forall f, g \in R[X], f = g) \land (\forall a, b \in R, a = b)$
Informal description
The zero polynomial $0 \in R[X]$ is monic if and only if all polynomials in $R[X]$ are equal and all elements in $R$ are equal.
Polynomial.Monic.as_sum theorem
(hp : p.Monic) : p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i
Full source 
theorem Monic.as_sum (hp : p.Monic) :
    p = X ^ p.natDegree + ∑ i ∈ range p.natDegree, C (p.coeff i) * X ^ i := by
  conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
  suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
  exact congr_arg C hp
Monic Polynomial Decomposition: $p = X^n + \sum_{i=0}^{n-1} a_i X^i$
Informal description
Let $p \in R[X]$ be a monic polynomial. Then $p$ can be expressed as the sum of the monomial $X^n$ (where $n$ is the degree of $p$) and a polynomial of degree less than $n$, i.e., \[ p = X^n + \sum_{i=0}^{n-1} a_i X^i \] where $a_i = p_i$ are the coefficients of $p$.
Polynomial.Monic.map theorem
[Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f)
Full source 
theorem Monic.map [Semiring S] (f : R →+* S) (hp : Monic p) : Monic (p.map f) := by
  unfold Monic
  nontriviality
  have : f p.leadingCoeff ≠ 0 := by
    rw [show _ = _ from hp, f.map_one]
    exact one_ne_zero
  rw [Polynomial.leadingCoeff, coeff_map]
  suffices p.coeff (p.map f).natDegree = 1 by simp [this]
  rwa [natDegree_eq_of_degree_eq (degree_map_eq_of_leadingCoeff_ne_zero f this)]
Monic Polynomials are Preserved under Ring Homomorphisms
Informal description
Let $R$ and $S$ be semirings, and let $f \colon R \to S$ be a ring homomorphism. If a polynomial $p \in R[X]$ is monic, then its image under the polynomial map induced by $f$ (denoted $p.map\, f$) is also monic in $S[X]$.
Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one theorem
{b : R} (hp : b * p.leadingCoeff = 1) : Monic (C b * p)
Full source 
theorem monic_C_mul_of_mul_leadingCoeff_eq_one {b : R} (hp : b * p.leadingCoeff = 1) :
    Monic (C b * p) := by
  unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]
Monicity of $C(b) \cdot p$ when $b \cdot \text{leadingCoeff}(p) = 1$
Informal description
Let $R$ be a semiring and $p \in R[X]$ be a polynomial. For any element $b \in R$ such that $b \cdot \text{leadingCoeff}(p) = 1$, the polynomial $C(b) \cdot p$ is monic, where $C(b)$ denotes the constant polynomial with coefficient $b$.
Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one theorem
{b : R} (hp : p.leadingCoeff * b = 1) : Monic (p * C b)
Full source 
theorem monic_mul_C_of_leadingCoeff_mul_eq_one {b : R} (hp : p.leadingCoeff * b = 1) :
    Monic (p * C b) := by
  unfold Monic
  nontriviality
  rw [leadingCoeff_mul' _] <;> simp [leadingCoeff_C b, hp]
Monicity of $p \cdot C(b)$ when leading coefficient times $b$ is 1
Informal description
Let $R$ be a semiring and $p \in R[X]$ be a polynomial. If there exists an element $b \in R$ such that the product of the leading coefficient of $p$ and $b$ equals $1$, then the polynomial $p \cdot C(b)$ is monic, where $C(b)$ denotes the constant polynomial $b$.
Polynomial.monic_of_degree_le theorem
(n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : Monic p
Full source 
theorem monic_of_degree_le (n : ℕ) (H1 : degree p ≤ n) (H2 : coeff p n = 1) : Monic p :=
  Decidable.byCases
    (fun H : degree p < n => eq_of_zero_eq_one (H2 ▸ (coeff_eq_zero_of_degree_lt H).symm) _ _)
    fun H : ¬degree p < n => by
    rwa [Monic, Polynomial.leadingCoeff, natDegree, (lt_or_eq_of_le H1).resolve_left H]
Monic Polynomial from Degree and Leading Coefficient Condition
Informal description
For a polynomial $p$ over a semiring $R$ and a natural number $n$, if the degree of $p$ is at most $n$ and the coefficient of $X^n$ in $p$ is $1$, then $p$ is monic.
Polynomial.monic_X_pow_add theorem
{n : ℕ} (H : degree p < n) : Monic (X ^ n + p)
Full source 
theorem monic_X_pow_add {n : ℕ} (H : degree p < n) : Monic (X ^ n + p) :=
  monic_of_degree_le n
    (le_trans (degree_add_le _ _) (max_le (degree_X_pow_le _) (le_of_lt H)))
    (by rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero])
Monicity of $X^n + p$ for $\deg(p) < n$
Informal description
For any polynomial $p$ over a semiring $R$ and a natural number $n$, if the degree of $p$ is strictly less than $n$, then the polynomial $X^n + p$ is monic.
Polynomial.Monic.mul theorem
(hp : Monic p) (hq : Monic q) : Monic (p * q)
Full source 
theorem Monic.mul (hp : Monic p) (hq : Monic q) : Monic (p * q) :=
  letI := Classical.decEq R
  if h0 : (0 : R) = 1 then
    haveI := subsingleton_of_zero_eq_one h0
    Subsingleton.elim _ _
  else by
    have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
      simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
    rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
Product of Monic Polynomials is Monic
Informal description
Let $p$ and $q$ be monic polynomials over a semiring $R$. Then the product $p \cdot q$ is also monic.
Polynomial.Monic.pow theorem
(hp : Monic p) : ∀ n : ℕ, Monic (p ^ n)
Full source 
theorem Monic.pow (hp : Monic p) : ∀ n : ℕ, Monic (p ^ n)
  | 0 => monic_one
  | n + 1 => by
    rw [pow_succ]
    exact (Monic.pow hp n).mul hp
Powers of Monic Polynomials are Monic
Informal description
If $p$ is a monic polynomial over a semiring $R$, then for any natural number $n$, the polynomial $p^n$ is also monic.
Polynomial.Monic.add_of_left theorem
(hp : Monic p) (hpq : degree q < degree p) : Monic (p + q)
Full source 
theorem Monic.add_of_left (hp : Monic p) (hpq : degree q < degree p) : Monic (p + q) := by
  rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]
Sum of Polynomials is Monic When Leading Term is Monic and Higher Degree
Informal description
Let $p$ and $q$ be polynomials over a semiring $R$ such that $p$ is monic and the degree of $q$ is strictly less than the degree of $p$. Then the sum $p + q$ is also monic.
Polynomial.Monic.add_of_right theorem
(hq : Monic q) (hpq : degree p < degree q) : Monic (p + q)
Full source 
theorem Monic.add_of_right (hq : Monic q) (hpq : degree p < degree q) : Monic (p + q) := by
  rwa [Monic, leadingCoeff_add_of_degree_lt hpq]
Sum of Polynomials is Monic When Higher-Degree Term is Monic
Informal description
Let $p$ and $q$ be polynomials over a semiring $R$ such that $q$ is monic and the degree of $p$ is strictly less than the degree of $q$. Then the sum $p + q$ is also monic.
Polynomial.Monic.of_mul_monic_left theorem
(hp : p.Monic) (hpq : (p * q).Monic) : q.Monic
Full source 
theorem Monic.of_mul_monic_left (hp : p.Monic) (hpq : (p * q).Monic) : q.Monic := by
  contrapose! hpq
  rw [Monic.def] at hpq ⊢
  rwa [leadingCoeff_monic_mul hp]
Monicity of Factor Given Monic Product
Informal description
Let $p$ and $q$ be polynomials over a semiring $R$. If $p$ is monic and the product $p \cdot q$ is monic, then $q$ is monic.
Polynomial.Monic.of_mul_monic_right theorem
(hq : q.Monic) (hpq : (p * q).Monic) : p.Monic
Full source 
theorem Monic.of_mul_monic_right (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic := by
  contrapose! hpq
  rw [Monic.def] at hpq ⊢
  rwa [leadingCoeff_mul_monic hq]
Monicity of Polynomial Factors When Product is Monic
Informal description
Let $p$ and $q$ be polynomials over a semiring $R$. If $q$ is monic and the product $p \cdot q$ is monic, then $p$ is monic.
Polynomial.Monic.comp theorem
(hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic
Full source 
lemma comp (hp : p.Monic) (hq : q.Monic) (h : q.natDegree ≠ 0) : (p.comp q).Monic := by
  nontriviality R
  have : (p.comp q).natDegree = p.natDegree * q.natDegree :=
    natDegree_comp_eq_of_mul_ne_zero <| by simp [hp.leadingCoeff, hq.leadingCoeff]
  rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
Composition of Monic Polynomials is Monic
Informal description
Let $p$ and $q$ be monic polynomials over a semiring $R$. If the degree of $q$ is nonzero, then the composition $p \circ q$ is also monic.
Polynomial.Monic.comp_X_add_C theorem
(hp : p.Monic) (r : R) : (p.comp (X + C r)).Monic
Full source 
lemma comp_X_add_C (hp : p.Monic) (r : R) : (p.comp (X + C r)).Monic := by
  nontriviality R
  refine hp.comp (monic_X_add_C _) fun ha ↦ ?_
  rw [natDegree_X_add_C] at ha
  exact one_ne_zero ha
Composition of Monic Polynomial with $X + r$ is Monic
Informal description
Let $p$ be a monic polynomial over a semiring $R$ and let $r \in R$. Then the composition $p(X + r)$ is also monic.
Polynomial.Monic.natDegree_eq_zero_iff_eq_one theorem
(hp : p.Monic) : p.natDegree = 0 ↔ p = 1
Full source 
@[simp]
theorem natDegree_eq_zero_iff_eq_one (hp : p.Monic) : p.natDegree = 0 ↔ p = 1 := by
  constructor <;> intro h
  swap
  · rw [h]
    exact natDegree_one
  have : p = C (p.coeff 0) := by
    rw [← Polynomial.degree_le_zero_iff]
    rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h
  rw [this]
  rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]
Monic Polynomial Has Degree Zero if and only if It is One
Informal description
Let $p$ be a monic polynomial over a semiring $R$. Then the natural degree of $p$ is zero if and only if $p$ is equal to the constant polynomial $1$.
Polynomial.Monic.degree_le_zero_iff_eq_one theorem
(hp : p.Monic) : p.degree ≤ 0 ↔ p = 1
Full source 
@[simp]
theorem degree_le_zero_iff_eq_one (hp : p.Monic) : p.degree ≤ 0 ↔ p = 1 := by
  rw [← hp.natDegree_eq_zero_iff_eq_one, natDegree_eq_zero_iff_degree_le_zero]
Degree Bound for Monic Polynomials: $\deg(p) \leq 0 \leftrightarrow p = 1$
Informal description
Let $p$ be a monic polynomial over a semiring $R$. Then the degree of $p$ is less than or equal to zero if and only if $p$ is equal to the constant polynomial $1$.
Polynomial.Monic.natDegree_mul theorem
(hp : p.Monic) (hq : q.Monic) : (p * q).natDegree = p.natDegree + q.natDegree
Full source 
theorem natDegree_mul (hp : p.Monic) (hq : q.Monic) :
    (p * q).natDegree = p.natDegree + q.natDegree := by
  nontriviality R
  apply natDegree_mul'
  simp [hp.leadingCoeff, hq.leadingCoeff]
Natural Degree of Product of Monic Polynomials is Sum of Degrees
Informal description
For two monic polynomials $p$ and $q$ over a semiring $R$, the natural degree of their product $p \cdot q$ is equal to the sum of their natural degrees, i.e., $\text{natDegree}(p \cdot q) = \text{natDegree}(p) + \text{natDegree}(q)$.
Polynomial.Monic.degree_mul_comm theorem
(hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).degree
Full source 
theorem degree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).degree = (q * p).degree := by
  by_cases h : q = 0
  · simp [h]
  rw [degree_mul', hp.degree_mul]
  · exact add_comm _ _
  · rwa [hp.leadingCoeff, one_mul, leadingCoeff_ne_zero]
Degree Commutativity for Products Involving Monic Polynomials
Informal description
For any monic polynomial $p$ and any polynomial $q$ over a semiring $R$, the degree of the product $p \cdot q$ is equal to the degree of the product $q \cdot p$, i.e., $\deg(p \cdot q) = \deg(q \cdot p)$.
Polynomial.Monic.natDegree_mul' theorem
(hp : p.Monic) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree
Full source 
nonrec theorem natDegree_mul' (hp : p.Monic) (hq : q ≠ 0) :
    (p * q).natDegree = p.natDegree + q.natDegree := by
  rw [natDegree_mul']
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
Natural Degree of Product of Monic and Nonzero Polynomials is Sum of Degrees
Informal description
For a monic polynomial $p$ and a nonzero polynomial $q$ over a semiring $R$, the natural degree of their product $p \cdot q$ is equal to the sum of their natural degrees, i.e., $\text{natDegree}(p \cdot q) = \text{natDegree}(p) + \text{natDegree}(q)$.
Polynomial.Monic.natDegree_mul_comm theorem
(hp : p.Monic) (q : R[X]) : (p * q).natDegree = (q * p).natDegree
Full source 
theorem natDegree_mul_comm (hp : p.Monic) (q : R[X]) : (p * q).natDegree = (q * p).natDegree := by
  by_cases h : q = 0
  · simp [h]
  rw [hp.natDegree_mul' h, Polynomial.natDegree_mul', add_comm]
  simpa [hp.leadingCoeff, leadingCoeff_ne_zero]
Natural Degree of Product of Monic Polynomial is Commutative
Informal description
For a monic polynomial $p$ and any polynomial $q$ over a semiring $R$, the natural degree of the product $p \cdot q$ is equal to the natural degree of the product $q \cdot p$, i.e., $\text{natDegree}(p \cdot q) = \text{natDegree}(q \cdot p)$.
Polynomial.Monic.not_dvd_of_natDegree_lt theorem
(hp : Monic p) (h0 : q ≠ 0) (hl : natDegree q < natDegree p) : ¬p ∣ q
Full source 
theorem not_dvd_of_natDegree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : natDegree q < natDegree p) :
    ¬p ∣ q := by
  rintro ⟨r, rfl⟩
  rw [hp.natDegree_mul' <| right_ne_zero_of_mul h0] at hl
  exact hl.not_le (Nat.le_add_right _ _)
Monic Polynomial Does Not Divide Polynomial of Smaller Degree
Informal description
Let $p$ be a monic polynomial and $q$ be a nonzero polynomial over a semiring $R$. If the natural degree of $q$ is strictly less than the natural degree of $p$, then $p$ does not divide $q$.
Polynomial.Monic.not_dvd_of_degree_lt theorem
(hp : Monic p) (h0 : q ≠ 0) (hl : degree q < degree p) : ¬p ∣ q
Full source 
theorem not_dvd_of_degree_lt (hp : Monic p) (h0 : q ≠ 0) (hl : degree q < degree p) : ¬p ∣ q :=
  Monic.not_dvd_of_natDegree_lt hp h0 <| natDegree_lt_natDegree h0 hl
Monic Polynomial Does Not Divide Polynomial of Smaller Degree
Informal description
Let $p$ be a monic polynomial and $q$ be a nonzero polynomial over a semiring $R$. If the degree of $q$ is strictly less than the degree of $p$, then $p$ does not divide $q$.
Polynomial.Monic.nextCoeff_mul theorem
(hp : Monic p) (hq : Monic q) : nextCoeff (p * q) = nextCoeff p + nextCoeff q
Full source 
theorem nextCoeff_mul (hp : Monic p) (hq : Monic q) :
    nextCoeff (p * q) = nextCoeff p + nextCoeff q := by
  nontriviality
  simp only [← coeff_one_reverse]
  rw [reverse_mul] <;> simp [hp.leadingCoeff, hq.leadingCoeff, mul_coeff_one, add_comm]
Next Coefficient of Product of Monic Polynomials: $\text{nextCoeff}(p \cdot q) = \text{nextCoeff}(p) + \text{nextCoeff}(q)$
Informal description
For any monic polynomials $p$ and $q$ over a semiring $R$, the next coefficient of their product $p \cdot q$ is equal to the sum of their next coefficients, i.e., \[ \text{nextCoeff}(p \cdot q) = \text{nextCoeff}(p) + \text{nextCoeff}(q). \]
Polynomial.Monic.nextCoeff_pow theorem
(hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff
Full source 
theorem nextCoeff_pow (hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff := by
  induction n with
  | zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
  | succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]
Next Coefficient of Power of Monic Polynomial: $\text{nextCoeff}(p^n) = n \cdot \text{nextCoeff}(p)$
Informal description
For any monic polynomial $p$ over a semiring $R$ and any natural number $n$, the next coefficient of $p^n$ is equal to $n$ times the next coefficient of $p$, i.e., \[ \text{nextCoeff}(p^n) = n \cdot \text{nextCoeff}(p). \]
Polynomial.Monic.natDegree_pow theorem
(hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree
Full source 
theorem natDegree_pow (hp : p.Monic) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree := by
  induction n with
  | zero => simp
  | succ n hn => rw [pow_succ, (hp.pow n).natDegree_mul hp, hn, Nat.succ_mul, add_comm]
Natural Degree of Powers of Monic Polynomials: $\text{natDegree}(p^n) = n \cdot \text{natDegree}(p)$
Informal description
For any monic polynomial $p$ over a semiring $R$ and any natural number $n$, the natural degree of $p^n$ is equal to $n$ times the natural degree of $p$, i.e., $\text{natDegree}(p^n) = n \cdot \text{natDegree}(p)$.
Polynomial.natDegree_pow_X_add_C theorem
[Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n
Full source 
@[simp]
theorem natDegree_pow_X_add_C [Nontrivial R] (n : ℕ) (r : R) : ((X + C r) ^ n).natDegree = n := by
  rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]
Natural degree of powers of $X + r$: $\text{natDegree}((X + r)^n) = n$
Informal description
Let $R$ be a nontrivial semiring. For any natural number $n$ and any element $r \in R$, the natural degree of the polynomial $(X + r)^n$ is equal to $n$.
Polynomial.monic_multiset_prod_of_monic theorem
(t : Multiset ι) (f : ι → R[X]) (ht : ∀ i ∈ t, Monic (f i)) : Monic (t.map f).prod
Full source 
theorem monic_multiset_prod_of_monic (t : Multiset ι) (f : ι → R[X]) (ht : ∀ i ∈ t, Monic (f i)) :
    Monic (t.map f).prod := by
  revert ht
  refine t.induction_on ?_ ?_; · simp
  intro a t ih ht
  rw [Multiset.map_cons, Multiset.prod_cons]
  exact (ht _ (Multiset.mem_cons_self _ _)).mul (ih fun _ hi => ht _ (Multiset.mem_cons_of_mem hi))
Product of Monic Polynomials over a Multiset is Monic
Informal description
Let $R$ be a commutative semiring and let $t$ be a multiset over an index type $\iota$. Given a family of polynomials $(f_i)_{i \in \iota}$ in $R[X]$ such that each $f_i$ is monic for all $i \in t$, then the product of the multiset obtained by mapping $f$ over $t$ is also monic. That is, if $f_i$ is monic for every $i \in t$, then $\prod_{i \in t} f_i$ is monic.
Polynomial.monic_prod_of_monic theorem
(s : Finset ι) (f : ι → R[X]) (hs : ∀ i ∈ s, Monic (f i)) : Monic (∏ i ∈ s, f i)
Full source 
theorem monic_prod_of_monic (s : Finset ι) (f : ι → R[X]) (hs : ∀ i ∈ s, Monic (f i)) :
    Monic (∏ i ∈ s, f i) :=
  monic_multiset_prod_of_monic s.1 f hs
Product of Monic Polynomials over a Finite Set is Monic
Informal description
Let $R$ be a commutative semiring and let $s$ be a finite set indexed by $\iota$. Given a family of polynomials $(f_i)_{i \in \iota}$ in $R[X]$ such that each $f_i$ is monic for all $i \in s$, then the product $\prod_{i \in s} f_i$ is also monic.
Polynomial.monic_finprod_of_monic theorem
(α : Type*) (f : α → R[X]) (hf : ∀ i ∈ Function.mulSupport f, Monic (f i)) : Monic (finprod f)
Full source 
theorem monic_finprod_of_monic (α : Type*) (f : α → R[X])
    (hf : ∀ i ∈ Function.mulSupport f, Monic (f i)) :
    Monic (finprod f) := by
  classical
  rw [finprod_def]
  split_ifs
  · exact monic_prod_of_monic _ _ fun a ha => hf a ((Set.Finite.mem_toFinset _).mp ha)
  · exact monic_one
Finitary Product of Monic Polynomials is Monic
Informal description
Let $R$ be a commutative semiring and let $f : \alpha \to R[X]$ be a function from a type $\alpha$ to the polynomial ring $R[X]$. If for every $i$ in the multiplicative support of $f$ (i.e., where $f(i) \neq 1$), the polynomial $f(i)$ is monic, then the finitary product $\prodᶠ_{i} f(i)$ is also monic.
Polynomial.Monic.nextCoeff_multiset_prod theorem
(t : Multiset ι) (f : ι → R[X]) (h : ∀ i ∈ t, Monic (f i)) : nextCoeff (t.map f).prod = (t.map fun i => nextCoeff (f i)).sum
Full source 
theorem Monic.nextCoeff_multiset_prod (t : Multiset ι) (f : ι → R[X]) (h : ∀ i ∈ t, Monic (f i)) :
    nextCoeff (t.map f).prod = (t.map fun i => nextCoeff (f i)).sum := by
  revert h
  refine Multiset.induction_on t ?_ fun a t ih ht => ?_
  · simp only [Multiset.not_mem_zero, forall_prop_of_true, forall_prop_of_false, Multiset.map_zero,
      Multiset.prod_zero, Multiset.sum_zero, not_false_iff, forall_true_iff]
    rw [← C_1]
    rw [nextCoeff_C_eq_zero]
  · rw [Multiset.map_cons, Multiset.prod_cons, Multiset.map_cons, Multiset.sum_cons,
      Monic.nextCoeff_mul, ih]
    exacts [fun i hi => ht i (Multiset.mem_cons_of_mem hi), ht a (Multiset.mem_cons_self _ _),
      monic_multiset_prod_of_monic _ _ fun b bs => ht _ (Multiset.mem_cons_of_mem bs)]
Next Coefficient of Product of Monic Polynomials over a Multiset Equals Sum of Next Coefficients
Informal description
Let $R$ be a commutative semiring and let $t$ be a multiset over an index type $\iota$. Given a family of monic polynomials $(f_i)_{i \in \iota}$ in $R[X]$, the next coefficient of the product $\prod_{i \in t} f_i$ is equal to the sum of the next coefficients of the polynomials $f_i$ for $i \in t$. That is, \[ \text{nextCoeff}\left(\prod_{i \in t} f_i\right) = \sum_{i \in t} \text{nextCoeff}(f_i). \]
Polynomial.Monic.nextCoeff_prod theorem
(s : Finset ι) (f : ι → R[X]) (h : ∀ i ∈ s, Monic (f i)) : nextCoeff (∏ i ∈ s, f i) = ∑ i ∈ s, nextCoeff (f i)
Full source 
theorem Monic.nextCoeff_prod (s : Finset ι) (f : ι → R[X]) (h : ∀ i ∈ s, Monic (f i)) :
    nextCoeff (∏ i ∈ s, f i) = ∑ i ∈ s, nextCoeff (f i) :=
  Monic.nextCoeff_multiset_prod s.1 f h
Next Coefficient of Product of Monic Polynomials over a Finite Set Equals Sum of Next Coefficients
Informal description
Let $R$ be a commutative semiring and let $s$ be a finite set over an index type $\iota$. Given a family of monic polynomials $(f_i)_{i \in \iota}$ in $R[X]$, the next coefficient of the product $\prod_{i \in s} f_i$ is equal to the sum of the next coefficients of the polynomials $f_i$ for $i \in s$. That is, \[ \text{nextCoeff}\left(\prod_{i \in s} f_i\right) = \sum_{i \in s} \text{nextCoeff}(f_i). \]
Polynomial.irreducible_of_monic theorem
(hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1
Full source 
lemma irreducible_of_monic (hp : p.Monic) (hp1 : p ≠ 1) :
    IrreducibleIrreducible p ↔ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f = 1 ∨ g = 1 := by
  refine
    ⟨fun h f g hf hg hp => (h.2 hp.symm).imp hf.eq_one_of_isUnit hg.eq_one_of_isUnit, fun h =>
      ⟨hp1 ∘ hp.eq_one_of_isUnit, fun f g hfg =>
        (h (g * C f.leadingCoeff) (f * C g.leadingCoeff) ?_ ?_ ?_).symm.imp
          (isUnit_of_mul_eq_one f _)
          (isUnit_of_mul_eq_one g _)⟩⟩
  · rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, mul_comm, ← hfg, ← Monic]
  · rwa [Monic, leadingCoeff_mul, leadingCoeff_C, ← leadingCoeff_mul, ← hfg, ← Monic]
  · rw [mul_mul_mul_comm, ← C_mul, ← leadingCoeff_mul, ← hfg, hp.leadingCoeff, C_1, mul_one,
      mul_comm, ← hfg]
Irreducibility Criterion for Monic Polynomials: $p$ irreducible iff all monic factorizations have a unit factor
Informal description
Let $p$ be a monic polynomial over a commutative semiring $R$ with $p \neq 1$. Then $p$ is irreducible if and only if for any monic polynomials $f, g \in R[X]$ such that $f \cdot g = p$, either $f = 1$ or $g = 1$.
Polynomial.Monic.irreducible_iff_natDegree theorem
(hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0
Full source 
lemma Monic.irreducible_iff_natDegree (hp : p.Monic) :
    IrreducibleIrreducible p ↔
      p ≠ 1 ∧ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → f.natDegree = 0 ∨ g.natDegree = 0 := by
  by_cases hp1 : p = 1; · simp [hp1]
  rw [irreducible_of_monic hp hp1, and_iff_right hp1]
  refine forall₄_congr fun a b ha hb => ?_
  rw [ha.natDegree_eq_zero_iff_eq_one, hb.natDegree_eq_zero_iff_eq_one]
Irreducibility Criterion for Monic Polynomials via Degree Constraints
Informal description
Let $p$ be a monic polynomial over a commutative semiring $R$. Then $p$ is irreducible if and only if $p \neq 1$ and for any monic polynomials $f, g \in R[X]$ such that $f \cdot g = p$, either $f$ or $g$ has degree zero (i.e., is a constant polynomial).
Polynomial.Monic.irreducible_iff_natDegree' theorem
(hp : p.Monic) : Irreducible p ↔ p ≠ 1 ∧ ∀ f g : R[X], f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2)
Full source 
lemma Monic.irreducible_iff_natDegree' (hp : p.Monic) : IrreducibleIrreducible p ↔ p ≠ 1 ∧
    ∀ f g : R[X], f.Monic → g.Monic → f * g = p → g.natDegree ∉ Ioc 0 (p.natDegree / 2) := by
  simp_rw [hp.irreducible_iff_natDegree, mem_Ioc, Nat.le_div_iff_mul_le zero_lt_two, mul_two]
  apply and_congr_right'
  constructor <;> intro h f g hf hg he <;> subst he
  · rw [hf.natDegree_mul hg, add_le_add_iff_right]
    exact fun ha => (h f g hf hg rfl).elim (ha.1.trans_le ha.2).ne' ha.1.ne'
  · simp_rw [hf.natDegree_mul hg, pos_iff_ne_zero] at h
    contrapose! h
    obtain hl | hl := le_total f.natDegree g.natDegree
    · exact ⟨g, f, hg, hf, mul_comm g f, h.1, add_le_add_left hl _⟩
    · exact ⟨f, g, hf, hg, rfl, h.2, add_le_add_right hl _⟩
Irreducibility Criterion for Monic Polynomials via Degree Bounds
Informal description
Let $p$ be a monic polynomial over a commutative semiring $R$. Then $p$ is irreducible if and only if $p \neq 1$ and for any monic polynomials $f, g \in R[X]$ such that $f \cdot g = p$, the degree of $g$ does not lie in the open-closed interval $(0, \deg(p)/2]$.
Polynomial.Monic.irreducible_iff_lt_natDegree_lt theorem
{p : R[X]} (hp : p.Monic) (hp1 : p ≠ 1) : Irreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬q ∣ p
Full source 
/-- Alternate phrasing of `Polynomial.Monic.irreducible_iff_natDegree'` where we only have to check
one divisor at a time. -/
lemma Monic.irreducible_iff_lt_natDegree_lt {p : R[X]} (hp : p.Monic) (hp1 : p ≠ 1) :
    IrreducibleIrreducible p ↔ ∀ q, Monic q → natDegree q ∈ Finset.Ioc 0 (natDegree p / 2) → ¬ q ∣ p := by
  rw [hp.irreducible_iff_natDegree', and_iff_right hp1]
  constructor
  · rintro h g hg hdg ⟨f, rfl⟩
    exact h f g (hg.of_mul_monic_left hp) hg (mul_comm f g) hdg
  · rintro h f g - hg rfl hdg
    exact h g hg hdg (dvd_mul_left g f)
Irreducibility Criterion for Monic Polynomials via Degree Constraints on Divisors
Informal description
Let $p$ be a monic polynomial over a commutative semiring $R$ with $p \neq 1$. Then $p$ is irreducible if and only if for every monic polynomial $q$ of degree $d$ satisfying $0 < d \leq \frac{1}{2}\deg(p)$, the polynomial $q$ does not divide $p$.
Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff theorem
(hm : p.Monic) (hnd : p.natDegree = 2) : ¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂
Full source 
lemma Monic.not_irreducible_iff_exists_add_mul_eq_coeff (hm : p.Monic) (hnd : p.natDegree = 2) :
    ¬Irreducible p¬Irreducible p ↔ ∃ c₁ c₂, p.coeff 0 = c₁ * c₂ ∧ p.coeff 1 = c₁ + c₂ := by
  cases subsingleton_or_nontrivial R
  · simp [natDegree_of_subsingleton] at hnd
  rw [hm.irreducible_iff_natDegree', and_iff_right, hnd]
  · push_neg
    constructor
    · rintro ⟨a, b, ha, hb, rfl, hdb⟩
      simp only [zero_lt_two, Nat.div_self, Nat.Ioc_succ_singleton, zero_add, mem_singleton] at hdb
      have hda := hnd
      rw [ha.natDegree_mul hb, hdb] at hda
      use a.coeff 0, b.coeff 0, mul_coeff_zero a b
      simpa only [nextCoeff, hnd, add_right_cancel hda, hdb] using ha.nextCoeff_mul hb
    · rintro ⟨c₁, c₂, hmul, hadd⟩
      refine
        ⟨X + C c₁, X + C c₂, monic_X_add_C _, monic_X_add_C _, ?_, ?_⟩
      · rw [p.as_sum_range_C_mul_X_pow, hnd, Finset.sum_range_succ, Finset.sum_range_succ,
          Finset.sum_range_one, ← hnd, hm.coeff_natDegree, hnd, hmul, hadd, C_mul, C_add, C_1]
        ring
      · rw [mem_Ioc, natDegree_X_add_C _]
        simp
  · rintro rfl
    simp [natDegree_one] at hnd
Characterization of Reducibility for Quadratic Monic Polynomials via Coefficients
Informal description
Let $p$ be a monic polynomial of degree 2 over a commutative semiring $R$. Then $p$ is not irreducible if and only if there exist elements $c_1, c_2 \in R$ such that: 1. The constant term of $p$ equals $c_1 \cdot c_2$, and 2. The coefficient of the linear term of $p$ equals $c_1 + c_2$.
Polynomial.Monic.natDegree_map theorem
[Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) : (P.map f).natDegree = P.natDegree
Full source 
@[simp]
theorem Monic.natDegree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
    (P.map f).natDegree = P.natDegree := by
  refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)
  rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
  exact one_ne_zero
Preservation of Natural Degree for Monic Polynomials under Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f \colon R \to S$ be a ring homomorphism. For any monic polynomial $P \in R[X]$, the natural degree of the polynomial $P$ is preserved under the map $f$, i.e., $\mathrm{natDegree}(P \cdot f) = \mathrm{natDegree}(P)$.
Polynomial.Monic.degree_map theorem
[Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) : (P.map f).degree = P.degree
Full source 
@[simp]
theorem Monic.degree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
    (P.map f).degree = P.degree := by
  by_cases hP : P = 0
  · simp [hP]
  · refine le_antisymm degree_map_le ?_
    rw [degree_eq_natDegree hP]
    refine le_degree_of_ne_zero ?_
    rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]
    exact one_ne_zero
Degree Preservation for Monic Polynomials under Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings with $S$ nontrivial, and let $f \colon R \to S$ be a ring homomorphism. For any monic polynomial $P \in R[X]$, the degree of the polynomial $P$ is preserved under the map $f$, i.e., $\deg(P \cdot f) = \deg(P)$.
Polynomial.degree_map_eq_of_injective theorem
(hf : Injective f) (p : R[X]) : degree (p.map f) = degree p
Full source 
theorem degree_map_eq_of_injective (hf : Injective f) (p : R[X]) : degree (p.map f) = degree p :=
  letI := Classical.decEq R
  if h : p = 0 then by simp [h]
  else
    degree_map_eq_of_leadingCoeff_ne_zero _
      (by rw [← f.map_zero]; exact mt hf.eq_iff.1 (mt leadingCoeff_eq_zero.1 h))
Degree Preservation under Injective Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings, and let $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the degree of the polynomial $p$ is preserved under the map $f$, i.e., $\deg(p \cdot f) = \deg(p)$.
Polynomial.natDegree_map_eq_of_injective theorem
(hf : Injective f) (p : R[X]) : natDegree (p.map f) = natDegree p
Full source 
theorem natDegree_map_eq_of_injective (hf : Injective f) (p : R[X]) :
    natDegree (p.map f) = natDegree p :=
  natDegree_eq_of_degree_eq (degree_map_eq_of_injective hf p)
Natural Degree Preservation under Injective Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the natural degree of $p$ is preserved under the map $f$, i.e., $\operatorname{natDegree}(p \cdot f) = \operatorname{natDegree}(p)$.
Polynomial.leadingCoeff_map' theorem
(hf : Injective f) (p : R[X]) : leadingCoeff (p.map f) = f (leadingCoeff p)
Full source 
theorem leadingCoeff_map' (hf : Injective f) (p : R[X]) :
    leadingCoeff (p.map f) = f (leadingCoeff p) := by
  unfold leadingCoeff
  rw [coeff_map, natDegree_map_eq_of_injective hf p]
Leading Coefficient Preservation under Injective Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the leading coefficient of the polynomial $p \cdot f$ is equal to $f$ applied to the leading coefficient of $p$, i.e., $\operatorname{leadingCoeff}(p \cdot f) = f(\operatorname{leadingCoeff}(p))$.
Polynomial.nextCoeff_map theorem
(hf : Injective f) (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff
Full source 
theorem nextCoeff_map (hf : Injective f) (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff := by
  unfold nextCoeff
  rw [natDegree_map_eq_of_injective hf]
  split_ifs <;> simp [*]
Next Coefficient Preservation under Injective Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the next coefficient of the polynomial $p \cdot f$ (the image of $p$ under $f$) is equal to $f$ applied to the next coefficient of $p$, i.e., $\operatorname{nextCoeff}(p \cdot f) = f(\operatorname{nextCoeff}(p))$.
Polynomial.leadingCoeff_of_injective theorem
(hf : Injective f) (p : R[X]) : leadingCoeff (p.map f) = f (leadingCoeff p)
Full source 
theorem leadingCoeff_of_injective (hf : Injective f) (p : R[X]) :
    leadingCoeff (p.map f) = f (leadingCoeff p) := by
  delta leadingCoeff
  rw [coeff_map f, natDegree_map_eq_of_injective hf p]
Leading Coefficient Preservation under Injective Ring Homomorphism
Informal description
Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, the leading coefficient of the mapped polynomial $p \cdot f$ is equal to $f$ applied to the leading coefficient of $p$, i.e., $\operatorname{leadingCoeff}(p \cdot f) = f(\operatorname{leadingCoeff}(p))$.
Polynomial.monic_of_injective theorem
(hf : Injective f) {p : R[X]} (hp : (p.map f).Monic) : p.Monic
Full source 
theorem monic_of_injective (hf : Injective f) {p : R[X]} (hp : (p.map f).Monic) : p.Monic := by
  apply hf
  rw [← leadingCoeff_of_injective hf, hp.leadingCoeff, f.map_one]
Monic Polynomials are Preserved under Injective Ring Homomorphisms
Informal description
Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, if the image polynomial $p \cdot f$ is monic (i.e., has leading coefficient 1), then $p$ itself is monic.
Function.Injective.monic_map_iff theorem
(hf : Injective f) {p : R[X]} : p.Monic ↔ (p.map f).Monic
Full source 
theorem _root_.Function.Injective.monic_map_iff (hf : Injective f) {p : R[X]} :
    p.Monic ↔ (p.map f).Monic :=
  ⟨Monic.map _, Polynomial.monic_of_injective hf⟩
Monic Polynomials are Preserved under Injective Ring Homomorphisms (Bidirectional)
Informal description
Let $R$ and $S$ be semirings and $f \colon R \to S$ be an injective ring homomorphism. For any polynomial $p \in R[X]$, $p$ is monic if and only if its image under the polynomial map induced by $f$ (denoted $p \cdot f$) is monic in $S[X]$.
Polynomial.monic_X_sub_C theorem
(x : R) : Monic (X - C x)
Full source 
theorem monic_X_sub_C (x : R) : Monic (X - C x) := by
  simpa only [sub_eq_add_neg, C_neg] using monic_X_add_C (-x)
Monicity of the Polynomial $X - x$
Informal description
For any element $x$ in a ring $R$, the polynomial $X - x$ is monic (i.e., its leading coefficient is 1).
Polynomial.monic_X_pow_sub theorem
{n : ℕ} (H : degree p < n) : Monic (X ^ n - p)
Full source 
theorem monic_X_pow_sub {n : ℕ} (H : degree p < n) : Monic (X ^ n - p) := by
  simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) < n by rwa [← degree_neg p] at H)
Monicity of $X^n - p$ for $\deg(p) < n$
Informal description
For any polynomial $p$ over a ring $R$ and a natural number $n$, if the degree of $p$ is strictly less than $n$, then the polynomial $X^n - p$ is monic.
Polynomial.monic_X_pow_sub_C theorem
{R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) : (X ^ n - C a).Monic
Full source 
/-- `X ^ n - a` is monic. -/
theorem monic_X_pow_sub_C {R : Type u} [Ring R] (a : R) {n : ℕ} (h : n ≠ 0) :
    (X ^ n - C a).Monic := by
  simpa only [map_neg, ← sub_eq_add_neg] using monic_X_pow_add_C (-a) h
Monicity of $X^n - a$ for $n \neq 0$
Informal description
For any ring $R$, element $a \in R$, and natural number $n \neq 0$, the polynomial $X^n - a$ is monic.
Polynomial.not_isUnit_X_pow_sub_one theorem
(R : Type*) [Ring R] [Nontrivial R] (n : ℕ) : ¬IsUnit (X ^ n - 1 : R[X])
Full source 
theorem not_isUnit_X_pow_sub_one (R : Type*) [Ring R] [Nontrivial R] (n : ℕ) :
    ¬IsUnit (X ^ n - 1 : R[X]) := by
  intro h
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp at h
  apply hn
  rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]
Non-unit Property of $X^n - 1$ in Polynomial Rings
Informal description
For any nontrivial ring $R$ and any natural number $n$, the polynomial $X^n - 1$ is not a unit in the polynomial ring $R[X]$.
Polynomial.Monic.comp_X_sub_C theorem
{p : R[X]} (hp : p.Monic) (r : R) : (p.comp (X - C r)).Monic
Full source 
lemma Monic.comp_X_sub_C {p : R[X]} (hp : p.Monic) (r : R) : (p.comp (X - C r)).Monic := by
  simpa using hp.comp_X_add_C (-r)
Monicity of $p(X - r)$ for monic $p$
Informal description
Let $p$ be a monic polynomial over a ring $R$ and let $r \in R$. Then the composition $p(X - r)$ is also monic.
Polynomial.Monic.sub_of_left theorem
{p q : R[X]} (hp : Monic p) (hpq : degree q < degree p) : Monic (p - q)
Full source 
theorem Monic.sub_of_left {p q : R[X]} (hp : Monic p) (hpq : degree q < degree p) :
    Monic (p - q) := by
  rw [sub_eq_add_neg]
  apply hp.add_of_left
  rwa [degree_neg]
Monicity Preservation under Subtraction of Lower Degree Polynomial
Informal description
Let $p$ and $q$ be polynomials over a ring $R$ such that $p$ is monic and the degree of $q$ is strictly less than the degree of $p$. Then the difference $p - q$ is also monic.
Polynomial.Monic.sub_of_right theorem
{p q : R[X]} (hq : q.leadingCoeff = -1) (hpq : degree p < degree q) : Monic (p - q)
Full source 
theorem Monic.sub_of_right {p q : R[X]} (hq : q.leadingCoeff = -1) (hpq : degree p < degree q) :
    Monic (p - q) := by
  have : (-q).coeff (-q).natDegree = 1 := by
    rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
  rw [sub_eq_add_neg]
  apply Monic.add_of_right this
  rwa [degree_neg]
Monicity of Polynomial Difference When Higher-Degree Term Has Leading Coefficient $-1$
Informal description
Let $p$ and $q$ be polynomials over a ring $R$ such that the leading coefficient of $q$ is $-1$ and the degree of $p$ is strictly less than the degree of $q$. Then the difference $p - q$ is monic.
Polynomial.Monic.mul_left_ne_zero theorem
(hp : Monic p) {q : R[X]} (hq : q ≠ 0) : q * p ≠ 0
Full source 
theorem Monic.mul_left_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : q * p ≠ 0 := by
  by_cases h : p = 1
  · simpa [h]
  rw [Ne, ← degree_eq_bot, hp.degree_mul, WithBot.add_eq_bot, not_or, degree_eq_bot]
  refine ⟨hq, ?_⟩
  rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
  refine (lt_trans ?_ h).ne'
  simp
Nonzero Product of Nonzero Polynomial with Monic Polynomial
Informal description
Let $p$ be a monic polynomial over a semiring $R$ and $q$ be a nonzero polynomial in $R[X]$. Then the product $q \cdot p$ is nonzero.
Polynomial.Monic.mul_right_ne_zero theorem
(hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q ≠ 0
Full source 
theorem Monic.mul_right_ne_zero (hp : Monic p) {q : R[X]} (hq : q ≠ 0) : p * q ≠ 0 := by
  by_cases h : p = 1
  · simpa [h]
  rw [Ne, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or,
    degree_eq_bot]
  refine ⟨hq, ?_⟩
  rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
  refine (lt_trans ?_ h).ne'
  simp
Nonvanishing of Product of Monic and Nonzero Polynomials
Informal description
Let $p$ be a monic polynomial over a semiring $R$ and $q$ be a nonzero polynomial in $R[X]$. Then the product $p \cdot q$ is nonzero.
Polynomial.Monic.mul_natDegree_lt_iff theorem
(h : Monic p) {q : R[X]} : (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0
Full source 
theorem Monic.mul_natDegree_lt_iff (h : Monic p) {q : R[X]} :
    (p * q).natDegree < p.natDegree ↔ p ≠ 1 ∧ q = 0 := by
  by_cases hq : q = 0
  · suffices 0 < p.natDegree ↔ p.natDegree ≠ 0 by simpa [hq, ← h.natDegree_eq_zero_iff_eq_one]
    exact ⟨fun h => h.ne', fun h => lt_of_le_of_ne (Nat.zero_le _) h.symm⟩
  · simp [h.natDegree_mul', hq]
Degree Inequality for Product of Monic and Zero Polynomials: $\text{natDegree}(p \cdot q) < \text{natDegree}(p) \leftrightarrow p \neq 1 \land q = 0$
Informal description
Let $p$ be a monic polynomial over a semiring $R$ and $q$ be a polynomial in $R[X]$. Then the natural degree of the product $p \cdot q$ is strictly less than the natural degree of $p$ if and only if $p$ is not the constant polynomial $1$ and $q$ is the zero polynomial. In other words, $\text{natDegree}(p \cdot q) < \text{natDegree}(p) \leftrightarrow p \neq 1 \land q = 0$.
Polynomial.Monic.mul_right_eq_zero_iff theorem
(h : Monic p) {q : R[X]} : p * q = 0 ↔ q = 0
Full source 
theorem Monic.mul_right_eq_zero_iff (h : Monic p) {q : R[X]} : p * q = 0 ↔ q = 0 := by
  by_cases hq : q = 0 <;> simp [h.mul_right_ne_zero, hq]
Vanishing of Product of Monic and Zero Polynomials: $p \cdot q = 0 \leftrightarrow q = 0$
Informal description
Let $p$ be a monic polynomial over a semiring $R$ and $q$ be a polynomial in $R[X]$. Then the product $p \cdot q$ is zero if and only if $q$ is zero.
Polynomial.Monic.mul_left_eq_zero_iff theorem
(h : Monic p) {q : R[X]} : q * p = 0 ↔ q = 0
Full source 
theorem Monic.mul_left_eq_zero_iff (h : Monic p) {q : R[X]} : q * p = 0 ↔ q = 0 := by
  by_cases hq : q = 0 <;> simp [h.mul_left_ne_zero, hq]
Zero Product Property for Monic Polynomials: $q \cdot p = 0 \leftrightarrow q = 0$
Informal description
Let $p$ be a monic polynomial over a semiring $R$ and $q$ be a polynomial in $R[X]$. Then the product $q \cdot p$ is zero if and only if $q$ is zero.
Polynomial.Monic.isRegular theorem
{R : Type*} [Ring R] {p : R[X]} (hp : Monic p) : IsRegular p
Full source 
theorem Monic.isRegular {R : Type*} [Ring R] {p : R[X]} (hp : Monic p) : IsRegular p := by
  constructor
  · intro q r h
    dsimp only at h
    rw [← sub_eq_zero, ← hp.mul_right_eq_zero_iff, mul_sub, h, sub_self]
  · intro q r h
    simp only at h
    rw [← sub_eq_zero, ← hp.mul_left_eq_zero_iff, sub_mul, h, sub_self]
Monic Polynomials are Regular in Polynomial Rings
Informal description
Let $R$ be a ring and $p \in R[X]$ be a monic polynomial. Then $p$ is a regular element in the polynomial ring $R[X]$, meaning that for any $q \in R[X]$, if $p \cdot q = 0$ or $q \cdot p = 0$, then $q = 0$.
Polynomial.degree_smul_of_smul_regular theorem
{S : Type*} [SMulZeroClass S R] {k : S} (p : R[X]) (h : IsSMulRegular R k) : (k • p).degree = p.degree
Full source 
theorem degree_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S}
    (p : R[X]) (h : IsSMulRegular R k) : (k • p).degree = p.degree := by
  refine le_antisymm ?_ ?_
  · rw [degree_le_iff_coeff_zero]
    intro m hm
    rw [degree_lt_iff_coeff_zero] at hm
    simp [hm m le_rfl]
  · rw [degree_le_iff_coeff_zero]
    intro m hm
    rw [degree_lt_iff_coeff_zero] at hm
    refine h ?_
    simpa using hm m le_rfl
Degree Preservation under Regular Scalar Multiplication in Polynomial Ring
Informal description
Let $R$ be a semiring and $S$ be a type equipped with a scalar multiplication action on $R$ that preserves zero. For any scalar $k \in S$ that is regular (i.e., the map $r \mapsto k \cdot r$ is injective on $R$) and any polynomial $p \in R[X]$, the degree of the scalar multiple $k \cdot p$ is equal to the degree of $p$.
Polynomial.natDegree_smul_of_smul_regular theorem
{S : Type*} [SMulZeroClass S R] {k : S} (p : R[X]) (h : IsSMulRegular R k) : (k • p).natDegree = p.natDegree
Full source 
theorem natDegree_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S}
    (p : R[X]) (h : IsSMulRegular R k) : (k • p).natDegree = p.natDegree := by
  by_cases hp : p = 0
  · simp [hp]
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree,
    degree_smul_of_smul_regular p h]
  contrapose! hp
  rw [← smul_zero k] at hp
  exact h.polynomial hp
Nat-degree Preservation under Regular Scalar Multiplication in Polynomial Ring
Informal description
Let $R$ be a semiring and $S$ be a type equipped with a scalar multiplication action on $R$ that preserves zero. For any scalar $k \in S$ that is $R$-regular (i.e., the map $r \mapsto k \cdot r$ is injective on $R$) and any polynomial $p \in R[X]$, the nat-degree of the scalar multiple $k \cdot p$ is equal to the nat-degree of $p$.
Polynomial.leadingCoeff_smul_of_smul_regular theorem
{S : Type*} [SMulZeroClass S R] {k : S} (p : R[X]) (h : IsSMulRegular R k) : (k • p).leadingCoeff = k • p.leadingCoeff
Full source 
theorem leadingCoeff_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S}
    (p : R[X]) (h : IsSMulRegular R k) : (k • p).leadingCoeff = k • p.leadingCoeff := by
  rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul,
    natDegree_smul_of_smul_regular p h]
Leading Coefficient Preservation under Regular Scalar Multiplication in Polynomial Ring
Informal description
Let $R$ be a semiring and $S$ be a type equipped with a scalar multiplication action on $R$ that preserves zero. For any scalar $k \in S$ that is $R$-regular (i.e., the map $r \mapsto k \cdot r$ is injective on $R$) and any polynomial $p \in R[X]$, the leading coefficient of the scalar multiple $k \cdot p$ is equal to $k$ multiplied by the leading coefficient of $p$.
Polynomial.monic_of_isUnit_leadingCoeff_inv_smul theorem
(h : IsUnit p.leadingCoeff) : Monic (h.unit⁻¹ • p)
Full source 
theorem monic_of_isUnit_leadingCoeff_inv_smul (h : IsUnit p.leadingCoeff) :
    Monic (h.unit⁻¹ • p) := by
  rw [Monic.def, leadingCoeff_smul_of_smul_regular _ (isSMulRegular_of_group _), Units.smul_def]
  obtain ⟨k, hk⟩ := h
  simp only [← hk, smul_eq_mul, ← Units.val_mul, Units.val_eq_one, inv_mul_eq_iff_eq_mul]
  simp [Units.ext_iff, IsUnit.unit_spec]
Monic Polynomial Construction via Unit Inversion
Informal description
Let $p$ be a polynomial over a semiring $R$ such that its leading coefficient is a unit in $R$. Then the polynomial obtained by multiplying $p$ by the inverse of this unit is monic, i.e., the leading coefficient of $h.unit⁻¹ \cdot p$ is $1$.
Polynomial.isUnit_leadingCoeff_mul_right_eq_zero_iff theorem
(h : IsUnit p.leadingCoeff) {q : R[X]} : p * q = 0 ↔ q = 0
Full source 
theorem isUnit_leadingCoeff_mul_right_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} :
    p * q = 0 ↔ q = 0 := by
  constructor
  · intro hp
    rw [← smul_eq_zero_iff_eq h.unit⁻¹] at hp
    have : h.unit⁻¹ • (p * q) = h.unit⁻¹ • p * q := by
      ext
      simp only [Units.smul_def, coeff_smul, coeff_mul, smul_eq_mul, mul_sum]
      refine sum_congr rfl fun x _ => ?_
      rw [← mul_assoc]
    rwa [this, Monic.mul_right_eq_zero_iff] at hp
    exact monic_of_isUnit_leadingCoeff_inv_smul _
  · rintro rfl
    simp
Vanishing of Product with Unit-Leading Polynomial: $p \cdot q = 0 \leftrightarrow q = 0$
Informal description
Let $p$ be a polynomial over a semiring $R$ such that its leading coefficient is a unit in $R$. Then for any polynomial $q \in R[X]$, the product $p \cdot q$ is zero if and only if $q$ is zero.
Polynomial.isUnit_leadingCoeff_mul_left_eq_zero_iff theorem
(h : IsUnit p.leadingCoeff) {q : R[X]} : q * p = 0 ↔ q = 0
Full source 
theorem isUnit_leadingCoeff_mul_left_eq_zero_iff (h : IsUnit p.leadingCoeff) {q : R[X]} :
    q * p = 0 ↔ q = 0 := by
  constructor
  · intro hp
    replace hp := congr_arg (· * C ↑h.unit⁻¹) hp
    simp only [zero_mul] at hp
    rwa [mul_assoc, Monic.mul_left_eq_zero_iff] at hp
    refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_
    simp [Units.mul_inv_eq_iff_eq_mul, IsUnit.unit_spec]
  · rintro rfl
    rw [zero_mul]
Zero Product Property for Polynomials with Unit Leading Coefficient: $q \cdot p = 0 \leftrightarrow q = 0$
Informal description
Let $R$ be a semiring and $p \in R[X]$ be a polynomial whose leading coefficient is a unit in $R$. Then for any polynomial $q \in R[X]$, the product $q \cdot p$ is zero if and only if $q$ is zero.