Mathlib.RingTheory.Polynomial.ScaleRoots

Polynomial.scaleRoots definition

(p : R[X]) (s : R) : R[X]

Full source

/-- `scaleRoots p s` is a polynomial with root `r * s` for each root `r` of `p`. -/
noncomputable def scaleRoots (p : R[X]) (s : R) : R[X] :=
  ∑ i ∈ p.support, monomial i (p.coeff i * s ^ (p.natDegree - i))

Scaling the roots of a polynomial

Informal description

Given a polynomial $ p $ over a ring $ R $ and an element $ s \in R $, the polynomial `scaleRoots p s` is defined as the polynomial whose roots are $ r \cdot s $ for each root $ r $ of $ p $. Explicitly, it is given by the sum \[ \sum_{i \in \text{supp}(p)} X^i \cdot (p_i \cdot s^{\deg p - i}), \] where $ p_i $ is the coefficient of $ X^i $ in $ p $ and $\text{supp}(p)$ is the set of indices where $ p $ has non-zero coefficients.

Polynomial.coeff_scaleRoots theorem

(p : R[X]) (s : R) (i : ℕ) : (scaleRoots p s).coeff i = coeff p i * s ^ (p.natDegree - i)

Full source

@[simp]
theorem coeff_scaleRoots (p : R[X]) (s : R) (i : ℕ) :
    (scaleRoots p s).coeff i = coeff p i * s ^ (p.natDegree - i) := by
  simp +contextual [scaleRoots, coeff_monomial]

Coefficient Formula for Scaled Roots Polynomial: $(\text{scaleRoots}\,p\,s)_i = p_i \cdot s^{\deg p - i}$

Informal description

For a polynomial $p$ over a ring $R$, an element $s \in R$, and a natural number $i$, the coefficient of $X^i$ in the scaled polynomial $\text{scaleRoots}\,p\,s$ is equal to the coefficient of $X^i$ in $p$ multiplied by $s$ raised to the power of the difference between the degree of $p$ and $i$, i.e., \[ (\text{scaleRoots}\,p\,s)_i = p_i \cdot s^{\deg p - i}. \]

Polynomial.coeff_scaleRoots_natDegree theorem

(p : R[X]) (s : R) : (scaleRoots p s).coeff p.natDegree = p.leadingCoeff

Full source

theorem coeff_scaleRoots_natDegree (p : R[X]) (s : R) :
    (scaleRoots p s).coeff p.natDegree = p.leadingCoeff := by
  rw [leadingCoeff, coeff_scaleRoots, tsub_self, pow_zero, mul_one]

Leading Coefficient Preservation under Root Scaling: $(\text{scaleRoots}\,p\,s)_{\deg p} = \text{lead}(p)$

Informal description

For any polynomial $p$ over a ring $R$ and any element $s \in R$, the coefficient of $X^{\deg p}$ in the scaled polynomial $\text{scaleRoots}\,p\,s$ equals the leading coefficient of $p$, i.e., \[ (\text{scaleRoots}\,p\,s)_{\deg p} = \text{lead}(p). \]

Polynomial.zero_scaleRoots theorem

(s : R) : scaleRoots 0 s = 0

Full source

@[simp]
theorem zero_scaleRoots (s : R) : scaleRoots 0 s = 0 := by
  ext
  simp

Scaling Roots of Zero Polynomial Yields Zero Polynomial

Informal description

For any element $s$ in a ring $R$, scaling the roots of the zero polynomial by $s$ yields the zero polynomial, i.e., $\text{scaleRoots}\,0\,s = 0$.

Polynomial.scaleRoots_ne_zero theorem

{p : R[X]} (hp : p ≠ 0) (s : R) : scaleRoots p s ≠ 0

Full source

theorem scaleRoots_ne_zero {p : R[X]} (hp : p ≠ 0) (s : R) : scaleRootsscaleRoots p s ≠ 0 := by
  intro h
  have : p.coeff p.natDegree ≠ 0 := mt leadingCoeff_eq_zero.mp hp
  have : (scaleRoots p s).coeff p.natDegree = 0 :=
    congr_fun (congr_arg (coeff : R[X] → ℕ → R) h) p.natDegree
  rw [coeff_scaleRoots_natDegree] at this
  contradiction

Nonzero Polynomial Remains Nonzero After Root Scaling

Informal description

For any nonzero polynomial $p$ over a ring $R$ and any element $s \in R$, the scaled polynomial $\text{scaleRoots}\,p\,s$ is also nonzero.

Polynomial.support_scaleRoots_le theorem

(p : R[X]) (s : R) : (scaleRoots p s).support ≤ p.support

Full source

theorem support_scaleRoots_le (p : R[X]) (s : R) : (scaleRoots p s).support ≤ p.support := by
  intro
  simpa using left_ne_zero_of_mul

Support of Scaled Roots Polynomial is Subset of Original Support

Informal description

For any polynomial $p$ over a ring $R$ and any element $s \in R$, the support of the scaled polynomial $\text{scaleRoots}\,p\,s$ is a subset of the support of $p$. In other words, if a term $X^i$ appears in $\text{scaleRoots}\,p\,s$, then it must also appear in $p$.

Polynomial.support_scaleRoots_eq theorem

(p : R[X]) {s : R} (hs : s ∈ nonZeroDivisors R) : (scaleRoots p s).support = p.support

Full source

theorem support_scaleRoots_eq (p : R[X]) {s : R} (hs : s ∈ nonZeroDivisors R) :
    (scaleRoots p s).support = p.support :=
  le_antisymm (support_scaleRoots_le p s)
    (by intro i
        simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
        intro p_ne_zero ps_zero
        have := pow_mem hs (p.natDegree - i) _ ps_zero
        contradiction)

Support Equality for Scaled Roots Polynomial with Non-Zero Divisor Scaling

Informal description

For a polynomial $p$ over a ring $R$ and an element $s \in R$ that is a non-zero divisor, the support of the scaled polynomial $\text{scaleRoots}\,p\,s$ is equal to the support of $p$. That is, the set of indices with non-zero coefficients remains unchanged after scaling the roots by $s$.

Polynomial.degree_scaleRoots theorem

(p : R[X]) {s : R} : degree (scaleRoots p s) = degree p

Full source

@[simp]
theorem degree_scaleRoots (p : R[X]) {s : R} : degree (scaleRoots p s) = degree p := by
  haveI := Classical.propDecidable
  by_cases hp : p = 0
  · rw [hp, zero_scaleRoots]
  refine le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree ?_)
  rw [coeff_scaleRoots_natDegree]
  intro h
  have := leadingCoeff_eq_zero.mp h
  contradiction

Degree Preservation under Root Scaling: $\deg(\text{scaleRoots}\,p\,s) = \deg(p)$

Informal description

For any polynomial $p$ over a ring $R$ and any element $s \in R$, the degree of the scaled polynomial $\text{scaleRoots}\,p\,s$ is equal to the degree of $p$, i.e., \[ \deg(\text{scaleRoots}\,p\,s) = \deg(p). \]

Polynomial.natDegree_scaleRoots theorem

(p : R[X]) (s : R) : natDegree (scaleRoots p s) = natDegree p

Full source

@[simp]
theorem natDegree_scaleRoots (p : R[X]) (s : R) : natDegree (scaleRoots p s) = natDegree p := by
  simp only [natDegree, degree_scaleRoots]

Natural Degree Preservation under Root Scaling: $\text{natDegree}(\text{scaleRoots}\,p\,s) = \text{natDegree}(p)$

Informal description

For any polynomial $p$ over a ring $R$ and any element $s \in R$, the natural degree of the scaled polynomial $\text{scaleRoots}\,p\,s$ is equal to the natural degree of $p$, i.e., \[ \text{natDegree}(\text{scaleRoots}\,p\,s) = \text{natDegree}(p). \]

Polynomial.monic_scaleRoots_iff theorem

{p : R[X]} (s : R) : Monic (scaleRoots p s) ↔ Monic p

Full source

theorem monic_scaleRoots_iff {p : R[X]} (s : R) : MonicMonic (scaleRoots p s) ↔ Monic p := by
  simp only [Monic, leadingCoeff, natDegree_scaleRoots, coeff_scaleRoots_natDegree]

Monicity Preservation under Root Scaling: $\text{scaleRoots}\,p\,s$ monic $\leftrightarrow p$ monic

Informal description

For any polynomial $p$ over a ring $R$ and any element $s \in R$, the scaled polynomial $\text{scaleRoots}\,p\,s$ is monic if and only if $p$ is monic. That is, \[ \text{scaleRoots}\,p\,s \text{ is monic} \leftrightarrow p \text{ is monic}. \]

Polynomial.map_scaleRoots theorem

(p : R[X]) (x : R) (f : R →+* S) (h : f p.leadingCoeff ≠ 0) : (p.scaleRoots x).map f = (p.map f).scaleRoots (f x)

Full source

theorem map_scaleRoots (p : R[X]) (x : R) (f : R →+* S) (h : f p.leadingCoeff ≠ 0) :
    (p.scaleRoots x).map f = (p.map f).scaleRoots (f x) := by
  ext
  simp [Polynomial.natDegree_map_of_leadingCoeff_ne_zero _ h]

Compatibility of Scaling Roots with Ring Homomorphisms: $f(\text{scaleRoots}\,p\,x) = \text{scaleRoots}\,(f(p))\,(f(x))$

Informal description

Let $p$ be a polynomial over a ring $R$, $x \in R$, and $f \colon R \to S$ a ring homomorphism such that $f$ does not annihilate the leading coefficient of $p$. Then, the image under $f$ of the polynomial obtained by scaling the roots of $p$ by $x$ is equal to the polynomial obtained by scaling the roots of $f(p)$ by $f(x)$. In other words, \[ f\big(\text{scaleRoots}\,p\,x\big) = \text{scaleRoots}\,(f(p))\,(f(x)). \]

Polynomial.scaleRoots_C theorem

(r c : R) : (C c).scaleRoots r = C c

Full source

@[simp]
lemma scaleRoots_C (r c : R) : (C c).scaleRoots r = C c := by
  ext; simp

Scaling Roots of Constant Polynomial Preserves It: $\text{scaleRoots}\,(C(c))\,r = C(c)$

Informal description

For any constant polynomial $C(c)$ over a ring $R$ and any element $r \in R$, scaling the roots of $C(c)$ by $r$ yields the same constant polynomial, i.e., $\text{scaleRoots}\,(C(c))\,r = C(c)$.

Polynomial.scaleRoots_one theorem

(p : R[X]) : p.scaleRoots 1 = p

Full source

@[simp]
lemma scaleRoots_one (p : R[X]) :
    p.scaleRoots 1 = p := by ext; simp

Identity Scaling of Polynomial Roots: $\text{scaleRoots}\,p\,1 = p$

Informal description

For any polynomial $p$ over a ring $R$, scaling its roots by the multiplicative identity $1$ yields the original polynomial, i.e., $\text{scaleRoots}\,p\,1 = p$.

Polynomial.scaleRoots_zero theorem

(p : R[X]) : p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree

Full source

@[simp]
lemma scaleRoots_zero (p : R[X]) :
    p.scaleRoots 0 = p.leadingCoeff • X ^ p.natDegree := by
  ext n
  simp only [coeff_scaleRoots, ne_eq, tsub_eq_zero_iff_le, not_le, zero_pow_eq, mul_ite,
    mul_one, mul_zero, coeff_smul, coeff_X_pow, smul_eq_mul]
  split_ifs with h₁ h₂ h₂
  · subst h₂; rfl
  · exact coeff_eq_zero_of_natDegree_lt (lt_of_le_of_ne h₁ (Ne.symm h₂))
  · exact (h₁ h₂.ge).elim
  · rfl

Scaling Roots by Zero Yields Leading Term Monomial: $\text{scaleRoots}\,p\,0 = c \cdot X^{\deg p}$

Informal description

For any polynomial $p$ over a ring $R$, scaling its roots by $0$ yields the monomial $c \cdot X^{\deg p}$, where $c$ is the leading coefficient of $p$. That is, \[ \text{scaleRoots}\,p\,0 = c \cdot X^{\deg p}. \]

Polynomial.one_scaleRoots theorem

(r : R) : (1 : R[X]).scaleRoots r = 1

Full source

@[simp]
lemma one_scaleRoots (r : R) :
    (1 : R[X]).scaleRoots r = 1 := by ext; simp

Scaling Roots of the Constant Polynomial: $\text{scaleRoots}\,1\,r = 1$

Informal description

For any element $r$ in a ring $R$, scaling the roots of the constant polynomial $1$ by $r$ yields the same constant polynomial $1$, i.e., $\text{scaleRoots}\,1\,r = 1$.

Polynomial.scaleRoots_eval₂_mul_of_commute theorem

 {p : S[X]} (f : S →+* A) (a : A) (s : S) (hsa : Commute (f s) a) (hf : ∀ s₁ s₂, Commute (f s₁) (f s₂)) :
  eval₂ f (f s * a) (scaleRoots p s) = f s ^ p.natDegree * eval₂ f a p

Full source

theorem scaleRoots_eval₂_mul_of_commute {p : S[X]} (f : S →+* A) (a : A) (s : S)
    (hsa : Commute (f s) a) (hf : ∀ s₁ s₂, Commute (f s₁) (f s₂)) :
    eval₂ f (f s * a) (scaleRoots p s) = f s ^ p.natDegree * eval₂ f a p := by
   calc
    _ = (scaleRoots p s).support.sum fun i =>
          f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i := by
      simp [eval₂_eq_sum, sum_def]
    _ = p.support.sum fun i => f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i :=
      (Finset.sum_subset (support_scaleRoots_le p s) fun i _hi hi' => by
        let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
        simp [this])
    _ = p.support.sum fun i : ℕ => f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i :=
      (Finset.sum_congr rfl fun i _hi => by
        simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc])
    _ = p.support.sum fun i : ℕ => f s ^ p.natDegree * (f (p.coeff i) * a ^ i) :=
      Finset.sum_congr rfl fun i hi => by
        rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]
        exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
    _ = f s ^ p.natDegree * eval₂ f a p := by simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

Evaluation of Scaled Roots Polynomial at Commuting Elements: $\text{eval}_2\,f\,(f(s) \cdot a)\,(\text{scaleRoots}\,p\,s) = f(s)^{\deg p} \cdot \text{eval}_2\,f\,a\,p$

Informal description

Let $p$ be a polynomial over a ring $S$, $f \colon S \to A$ a ring homomorphism, $a \in A$ an element, and $s \in S$ such that $f(s)$ and $a$ commute (i.e., $f(s) \cdot a = a \cdot f(s)$). Suppose further that $f$ preserves commutativity (i.e., for any $s_1, s_2 \in S$, $f(s_1)$ and $f(s_2)$ commute). Then evaluating the scaled polynomial $\text{scaleRoots}\,p\,s$ at $f(s) \cdot a$ via $f$ yields: \[ \text{eval}_2\,f\,(f(s) \cdot a)\,(\text{scaleRoots}\,p\,s) = f(s)^{\deg p} \cdot \text{eval}_2\,f\,a\,p. \]

Polynomial.scaleRoots_eval₂_mul theorem

{p : S[X]} (f : S →+* R) (r : R) (s : S) : eval₂ f (f s * r) (scaleRoots p s) = f s ^ p.natDegree * eval₂ f r p

Full source

theorem scaleRoots_eval₂_mul {p : S[X]} (f : S →+* R) (r : R) (s : S) :
    eval₂ f (f s * r) (scaleRoots p s) = f s ^ p.natDegree * eval₂ f r p :=
  scaleRoots_eval₂_mul_of_commute f r s (mul_comm _ _) fun _ _ ↦ mul_comm _ _

Evaluation of Scaled Roots Polynomial: $\text{eval}_2\,f\,(f(s) \cdot r)\,(\text{scaleRoots}\,p\,s) = f(s)^{\deg p} \cdot \text{eval}_2\,f\,r\,p$

Informal description

Let $p$ be a polynomial over a ring $S$, $f \colon S \to R$ a ring homomorphism, $r \in R$ an element, and $s \in S$. Then evaluating the scaled polynomial $\text{scaleRoots}\,p\,s$ at $f(s) \cdot r$ via $f$ yields: \[ \text{eval}_2\,f\,(f(s) \cdot r)\,(\text{scaleRoots}\,p\,s) = f(s)^{\deg p} \cdot \text{eval}_2\,f\,r\,p. \]

Polynomial.scaleRoots_eval₂_eq_zero theorem

{p : S[X]} (f : S →+* R) {r : R} {s : S} (hr : eval₂ f r p = 0) : eval₂ f (f s * r) (scaleRoots p s) = 0

Full source

theorem scaleRoots_eval₂_eq_zero {p : S[X]} (f : S →+* R) {r : R} {s : S} (hr : eval₂ f r p = 0) :
    eval₂ f (f s * r) (scaleRoots p s) = 0 := by rw [scaleRoots_eval₂_mul, hr, mul_zero]

Root Scaling Property: $\text{eval}_2\,f\,(f(s) \cdot r)\,(\text{scaleRoots}\,p\,s) = 0$ when $\text{eval}_2\,f\,r\,p = 0$

Informal description

Let $p$ be a polynomial over a ring $S$, $f \colon S \to R$ a ring homomorphism, $r \in R$, and $s \in S$. If $r$ is a root of $p$ under the evaluation map $\text{eval}_2\,f$ (i.e., $\text{eval}_2\,f\,r\,p = 0$), then $f(s) \cdot r$ is a root of the scaled polynomial $\text{scaleRoots}\,p\,s$, i.e., \[ \text{eval}_2\,f\,(f(s) \cdot r)\,(\text{scaleRoots}\,p\,s) = 0. \]

Polynomial.scaleRoots_aeval_eq_zero theorem

[Algebra R A] {p : R[X]} {a : A} {r : R} (ha : aeval a p = 0) : aeval (algebraMap R A r * a) (scaleRoots p r) = 0

Full source

theorem scaleRoots_aeval_eq_zero [Algebra R A] {p : R[X]} {a : A} {r : R} (ha : aeval a p = 0) :
    aeval (algebraMap R A r * a) (scaleRoots p r) = 0 := by
  rw [aeval_def, scaleRoots_eval₂_mul_of_commute, ← aeval_def, ha, mul_zero]
  · apply Algebra.commutes
  · intros; rw [Commute, SemiconjBy, ← map_mul, ← map_mul, mul_comm]

Root Scaling Property: $\text{aeval}\,(r \cdot a)\,(\text{scaleRoots}\,p\,r) = 0$ when $\text{aeval}\,a\,p = 0$

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any polynomial $p \in R[X]$, element $a \in A$, and $r \in R$, if $a$ is a root of $p$ (i.e., $\text{aeval}\,a\,p = 0$), then $r \cdot a$ is a root of the scaled polynomial $\text{scaleRoots}\,p\,r$, i.e., \[ \text{aeval}\,(r \cdot a)\,(\text{scaleRoots}\,p\,r) = 0. \]

Polynomial.scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero theorem

 {p : S[X]} {f : S →+* K} (hf : Function.Injective f) {r s : S} (hr : eval₂ f (f r / f s) p = 0)
  (hs : s ∈ nonZeroDivisors S) : eval₂ f (f r) (scaleRoots p s) = 0

Full source

theorem scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero {p : S[X]} {f : S →+* K}
    (hf : Function.Injective f) {r s : S} (hr : eval₂ f (f r / f s) p = 0)
    (hs : s ∈ nonZeroDivisors S) : eval₂ f (f r) (scaleRoots p s) = 0 := by
  -- if we don't specify the type with `(_ : S)`, the proof is much slower
  nontriviality S using Subsingleton.eq_zero (_ : S)
  convert @scaleRoots_eval₂_eq_zero _ _ _ _ p f _ s hr
  rw [← mul_div_assoc, mul_comm, mul_div_cancel_right₀]
  exact map_ne_zero_of_mem_nonZeroDivisors _ hf hs

Root Scaling Property for Fractional Roots: $\text{eval}_2\,f\,(f(r))\,(\text{scaleRoots}\,p\,s) = 0$ when $\text{eval}_2\,f\,(\frac{f(r)}{f(s)})\,p = 0$ and $s$ is a non-zero divisor

Informal description

Let $p$ be a polynomial over a ring $S$, $f \colon S \to K$ an injective ring homomorphism, and $r, s \in S$ with $s$ a non-zero divisor. If $\frac{f(r)}{f(s)}$ is a root of $p$ under the evaluation map $\text{eval}_2\,f$ (i.e., $\text{eval}_2\,f\,(\frac{f(r)}{f(s)})\,p = 0$), then $f(r)$ is a root of the scaled polynomial $\text{scaleRoots}\,p\,s$, i.e., \[ \text{eval}_2\,f\,(f(r))\,(\text{scaleRoots}\,p\,s) = 0. \]

Polynomial.scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero theorem

 [Algebra R K] (inj : Function.Injective (algebraMap R K)) {p : R[X]} {r s : R}
  (hr : aeval (algebraMap R K r / algebraMap R K s) p = 0) (hs : s ∈ nonZeroDivisors R) :
  aeval (algebraMap R K r) (scaleRoots p s) = 0

Full source

theorem scaleRoots_aeval_eq_zero_of_aeval_div_eq_zero [Algebra R K]
    (inj : Function.Injective (algebraMap R K)) {p : R[X]} {r s : R}
    (hr : aeval (algebraMap R K r / algebraMap R K s) p = 0) (hs : s ∈ nonZeroDivisors R) :
    aeval (algebraMap R K r) (scaleRoots p s) = 0 :=
  scaleRoots_eval₂_eq_zero_of_eval₂_div_eq_zero inj hr hs

Root Scaling Property for Fractional Roots in Algebras: $\text{aeval}\,(r)\,(\text{scaleRoots}\,p\,s) = 0$ when $\text{aeval}\,(\frac{r}{s})\,p = 0$ and $s$ is a non-zero divisor

Informal description

Let $R$ be a commutative ring and $K$ an $R$-algebra with an injective algebra map $\text{algebraMap}\,R\,K$. For any polynomial $p \in R[X]$ and elements $r, s \in R$ where $s$ is a non-zero divisor, if $\frac{\text{algebraMap}\,R\,K\,r}{\text{algebraMap}\,R\,K\,s}$ is a root of $p$ under the evaluation map $\text{aeval}$ (i.e., $\text{aeval}\,(\frac{\text{algebraMap}\,R\,K\,r}{\text{algebraMap}\,R\,K\,s})\,p = 0$), then $\text{algebraMap}\,R\,K\,r$ is a root of the scaled polynomial $\text{scaleRoots}\,p\,s$, i.e., \[ \text{aeval}\,(\text{algebraMap}\,R\,K\,r)\,(\text{scaleRoots}\,p\,s) = 0. \]

Polynomial.scaleRoots_mul theorem

(p : R[X]) (r s) : p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s

Full source

@[simp]
lemma scaleRoots_mul (p : R[X]) (r s) :
    p.scaleRoots (r * s) = (p.scaleRoots r).scaleRoots s := by
  ext; simp [mul_pow, mul_assoc]

Composition of Root Scaling: $\text{scaleRoots}\,p\,(r \cdot s) = \text{scaleRoots}\,(\text{scaleRoots}\,p\,r)\,s$

Informal description

For any polynomial $p$ over a ring $R$ and any elements $r, s \in R$, scaling the roots of $p$ by the product $r \cdot s$ is equivalent to first scaling the roots by $r$ and then scaling the resulting polynomial's roots by $s$. That is, \[ \text{scaleRoots}\,p\,(r \cdot s) = \text{scaleRoots}\,(\text{scaleRoots}\,p\,r)\,s. \]

Polynomial.mul_scaleRoots theorem

 (p q : R[X]) (r : R) :
  r ^ (natDegree p + natDegree q - natDegree (p * q)) • (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Full source

/-- Multiplication and `scaleRoots` commute up to a power of `r`. The factor disappears if we
assume that the product of the leading coeffs does not vanish. See `Polynomial.mul_scaleRoots'`. -/
lemma mul_scaleRoots (p q : R[X]) (r : R) :
    r ^ (natDegree p + natDegree q - natDegree (p * q)) • (p * q).scaleRoots r =
      p.scaleRoots r * q.scaleRoots r := by
  ext n; simp only [coeff_scaleRoots, coeff_smul, smul_eq_mul]
  trans (∑ x ∈ Finset.antidiagonal n, coeff p x.1 * coeff q x.2) *
    r ^ (natDegree p + natDegree q - n)
  · rw [← coeff_mul]
    cases lt_or_le (natDegree (p * q)) n with
    | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
    | inr h =>
      rw [mul_comm, mul_assoc, ← pow_add, add_comm, tsub_add_tsub_cancel natDegree_mul_le h]
  · rw [coeff_mul, Finset.sum_mul]
    apply Finset.sum_congr rfl
    simp only [Finset.mem_antidiagonal, coeff_scaleRoots, Prod.forall]
    intros a b e
    cases lt_or_le (natDegree p) a with
    | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
    | inr ha =>
      cases lt_or_le (natDegree q) b with
      | inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul, mul_zero]
      | inr hb =>
        simp only [← e, mul_assoc, mul_comm (r ^ (_ - a)), ← pow_add]
        rw [add_comm (_ - _), tsub_add_tsub_comm ha hb]

Scaling Roots of Product Polynomials: $r^{\deg p + \deg q - \deg(pq)} \cdot \text{scaleRoots}(pq, r) = \text{scaleRoots}(p, r) \cdot \text{scaleRoots}(q, r)$

Informal description

Let $p$ and $q$ be polynomials over a ring $R$, and let $r \in R$. Then \[ r^{\deg p + \deg q - \deg(pq)} \cdot \text{scaleRoots}(pq, r) = \text{scaleRoots}(p, r) \cdot \text{scaleRoots}(q, r), \] where $\text{scaleRoots}(p, r)$ denotes the polynomial obtained by scaling the roots of $p$ by $r$.

Polynomial.mul_scaleRoots' theorem

 (p q : R[X]) (r : R) (h : leadingCoeff p * leadingCoeff q ≠ 0) : (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Full source

lemma mul_scaleRoots' (p q : R[X]) (r : R) (h : leadingCoeffleadingCoeff p * leadingCoeff q ≠ 0) :
    (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r := by
  rw [← mul_scaleRoots, natDegree_mul' h, tsub_self, pow_zero, one_smul]

Scaling Roots of Product Polynomials with Nonzero Leading Coefficients: $\text{scaleRoots}(pq, r) = \text{scaleRoots}(p, r) \cdot \text{scaleRoots}(q, r)$

Informal description

Let $p$ and $q$ be polynomials over a ring $R$, and let $r \in R$. If the product of the leading coefficients of $p$ and $q$ is nonzero, then the polynomial obtained by scaling the roots of $p * q$ by $r$ equals the product of the polynomials obtained by scaling the roots of $p$ and $q$ individually by $r$, i.e., \[ \text{scaleRoots}(p * q, r) = \text{scaleRoots}(p, r) * \text{scaleRoots}(q, r). \]

Polynomial.mul_scaleRoots_of_noZeroDivisors theorem

(p q : R[X]) (r : R) [NoZeroDivisors R] : (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r

Full source

lemma mul_scaleRoots_of_noZeroDivisors (p q : R[X]) (r : R) [NoZeroDivisors R] :
    (p * q).scaleRoots r = p.scaleRoots r * q.scaleRoots r := by
  by_cases hp : p = 0; · simp [hp]
  by_cases hq : q = 0; · simp [hq]
  apply mul_scaleRoots'
  simp only [ne_eq, mul_eq_zero, leadingCoeff_eq_zero, hp, hq, or_self, not_false_eq_true]

Scaling Roots of Product Polynomials in a Domain: $\text{scaleRoots}(pq, r) = \text{scaleRoots}(p, r) \cdot \text{scaleRoots}(q, r)$

Informal description

Let $R$ be a ring with no zero divisors, and let $p, q$ be polynomials over $R$. For any element $r \in R$, the polynomial obtained by scaling the roots of the product $p \cdot q$ by $r$ equals the product of the polynomials obtained by scaling the roots of $p$ and $q$ individually by $r$, i.e., \[ \text{scaleRoots}(p \cdot q, r) = \text{scaleRoots}(p, r) \cdot \text{scaleRoots}(q, r). \]

Polynomial.add_scaleRoots_of_natDegree_eq theorem

 (p q : R[X]) (r : R) (h : natDegree p = natDegree q) :
  r ^ (natDegree p - natDegree (p + q)) • (p + q).scaleRoots r = p.scaleRoots r + q.scaleRoots r

Full source

lemma add_scaleRoots_of_natDegree_eq (p q : R[X]) (r : R) (h : natDegree p = natDegree q) :
    r ^ (natDegree p - natDegree (p + q)) • (p + q).scaleRoots r =
      p.scaleRoots r + q.scaleRoots r := by
  ext n; simp only [coeff_smul, coeff_scaleRoots, coeff_add, smul_eq_mul,
    mul_comm (r ^ _), ← pow_add, ← h, ← add_mul, add_comm (_ - n)]
  #adaptation_note /-- v4.7.0-rc1
  Previously `mul_assoc` was part of the `simp only` above, and this `rw` was not needed.
  but this now causes a max rec depth error. -/
  rw [mul_assoc, ← pow_add]
  cases lt_or_le (natDegree (p + q)) n with
  | inl hn => simp only [← coeff_add, coeff_eq_zero_of_natDegree_lt hn, zero_mul]
  | inr hn =>
      rw [add_comm (_ - n), tsub_add_tsub_cancel (natDegree_add_le_of_degree_le le_rfl h.ge) hn]

Scaling Roots Preserves Addition for Equal-Degree Polynomials: $r^{\deg p - \deg(p+q)} \cdot \text{scaleRoots}(p+q, r) = \text{scaleRoots}(p, r) + \text{scaleRoots}(q, r)$

Informal description

Let $p$ and $q$ be polynomials over a ring $R$, and let $r \in R$. If $p$ and $q$ have the same degree, then: \[ r^{\deg p - \deg(p + q)} \cdot \text{scaleRoots}(p + q, r) = \text{scaleRoots}(p, r) + \text{scaleRoots}(q, r), \] where $\text{scaleRoots}(p, r)$ denotes the polynomial obtained by scaling the roots of $p$ by $r$.

Polynomial.scaleRoots_dvd' theorem

(p q : R[X]) {r : R} (hr : IsUnit r) (hpq : p ∣ q) : p.scaleRoots r ∣ q.scaleRoots r

Full source

lemma scaleRoots_dvd' (p q : R[X]) {r : R} (hr : IsUnit r)
    (hpq : p ∣ q) : p.scaleRoots r ∣ q.scaleRoots r := by
  obtain ⟨a, rfl⟩ := hpq
  rw [← ((hr.pow (natDegree p + natDegree a - natDegree (p * a))).map
    (algebraMap R R[X])).dvd_mul_left, ← Algebra.smul_def, mul_scaleRoots]
  exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Divisibility of Scaled Polynomials by Units: $\text{scaleRoots}(p, r) \mid \text{scaleRoots}(q, r)$ when $p \mid q$ and $r$ is a unit

Informal description

Let $p$ and $q$ be polynomials over a ring $R$, and let $r \in R$ be a unit. If $p$ divides $q$, then the scaled polynomial $\text{scaleRoots}(p, r)$ divides $\text{scaleRoots}(q, r)$.

Polynomial.scaleRoots_dvd theorem

(p q : R[X]) {r : R} [NoZeroDivisors R] (hpq : p ∣ q) : p.scaleRoots r ∣ q.scaleRoots r

Full source

lemma scaleRoots_dvd (p q : R[X]) {r : R} [NoZeroDivisors R] (hpq : p ∣ q) :
    p.scaleRoots r ∣ q.scaleRoots r := by
  obtain ⟨a, rfl⟩ := hpq
  rw [mul_scaleRoots_of_noZeroDivisors]
  exact dvd_mul_right (scaleRoots p r) (scaleRoots a r)

Divisibility of Scaled Polynomials in a Domain: $\text{scaleRoots}(p, r) \mid \text{scaleRoots}(q, r)$ when $p \mid q$

Informal description

Let $R$ be a ring with no zero divisors, and let $p$ and $q$ be polynomials over $R$. For any element $r \in R$, if $p$ divides $q$, then the polynomial obtained by scaling the roots of $p$ by $r$ divides the polynomial obtained by scaling the roots of $q$ by $r$, i.e., \[ \text{scaleRoots}(p, r) \mid \text{scaleRoots}(q, r). \]

Polynomial.scaleRoots_dvd_iff theorem

(p q : R[X]) {r : R} (hr : IsUnit r) : p.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q

Full source

lemma scaleRoots_dvd_iff (p q : R[X]) {r : R} (hr : IsUnit r) :
    p.scaleRoots r ∣ q.scaleRoots rp.scaleRoots r ∣ q.scaleRoots r ↔ p ∣ q := by
  refine ⟨?_ ∘ scaleRoots_dvd' _ _ (hr.unit⁻¹).isUnit, scaleRoots_dvd' p q hr⟩
  simp [← scaleRoots_mul, scaleRoots_one]

Divisibility Equivalence for Scaled Polynomials: $\text{scaleRoots}(p, r) \mid \text{scaleRoots}(q, r) \leftrightarrow p \mid q$ for unit $r$

Informal description

Let $p$ and $q$ be polynomials over a ring $R$, and let $r \in R$ be a unit. Then the scaled polynomial $\text{scaleRoots}(p, r)$ divides $\text{scaleRoots}(q, r)$ if and only if $p$ divides $q$.

Polynomial.isCoprime_scaleRoots theorem

(p q : R[X]) (r : R) (hr : IsUnit r) (h : IsCoprime p q) : IsCoprime (p.scaleRoots r) (q.scaleRoots r)

Full source

lemma isCoprime_scaleRoots (p q : R[X]) (r : R) (hr : IsUnit r) (h : IsCoprime p q) :
    IsCoprime (p.scaleRoots r) (q.scaleRoots r) := by
  obtain ⟨a, b, e⟩ := h
  let s : R := ↑hr.unit⁻¹
  have : natDegree (a * p) = natDegree (b * q) := by
    apply natDegree_eq_of_natDegree_add_eq_zero
    rw [e, natDegree_one]
  use s ^ natDegree (a * p) • s ^ (natDegree a + natDegree p - natDegree (a * p)) • a.scaleRoots r
  use s ^ natDegree (a * p) • s ^ (natDegree b + natDegree q - natDegree (b * q)) • b.scaleRoots r
  simp only [s, smul_mul_assoc, ← mul_scaleRoots, smul_smul, Units.smul_def, mul_assoc,
    ← mul_pow, IsUnit.val_inv_mul, one_pow, mul_one, ← smul_add, one_smul, e, natDegree_one,
    one_scaleRoots, ← add_scaleRoots_of_natDegree_eq _ _ _ this, tsub_zero]

Coprimality is preserved under root scaling: $\text{IsCoprime}(p, q) \Rightarrow \text{IsCoprime}(\text{scaleRoots}(p, r), \text{scaleRoots}(q, r))$ for unit $r$

Informal description

Let $p$ and $q$ be polynomials over a ring $R$, and let $r \in R$ be a unit. If $p$ and $q$ are coprime, then the scaled polynomials $\text{scaleRoots}(p, r)$ and $\text{scaleRoots}(q, r)$ are also coprime.