doc-next-gen

Mathlib.Algebra.Polynomial.Expand

Module docstring

{"# Expand a polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

Main definitions

  • Polynomial.expand R p f: expand the polynomial f with coefficients in a commutative semiring R by a factor of p, so expand R p (∑ aₙ xⁿ) is ∑ aₙ xⁿᵖ.
  • Polynomial.contract p f: the opposite of expand, so it sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.

"}

Polynomial.expand definition
: R[X] →ₐ[R] R[X]
Full source 
/-- Expand the polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`. -/
noncomputable def expand : R[X]R[X] →ₐ[R] R[X] :=
  { (eval₂RingHom C (X ^ p) : R[X]R[X] →+* R[X]) with commutes' := fun _ => eval₂_C _ _ }
Polynomial expansion by $p$-th power
Informal description
Given a commutative semiring $R$ and a natural number $p$, the function $\text{expand}_R p$ maps a polynomial $f = \sum a_n X^n \in R[X]$ to the polynomial $\sum a_n X^{n p} \in R[X]$. This is an $R$-algebra homomorphism from $R[X]$ to itself.
Polynomial.coe_expand theorem
: (expand R p : R[X] → R[X]) = eval₂ C (X ^ p)
Full source 
theorem coe_expand : (expand R p : R[X] → R[X]) = eval₂ C (X ^ p) :=
  rfl
Expansion as Evaluation at $X^p$
Informal description
The polynomial expansion function $\text{expand}_R p$ is equal to the evaluation of the polynomial at $X^p$ using the constant polynomial embedding $C$, i.e., $\text{expand}_R p(f) = \text{eval}_2 C (X^p)(f)$ for any polynomial $f \in R[X]$.
Polynomial.expand_eq_comp_X_pow theorem
{f : R[X]} : expand R p f = f.comp (X ^ p)
Full source 
theorem expand_eq_comp_X_pow {f : R[X]} : expand R p f = f.comp (X ^ p) := rfl
Expansion as Composition with $X^p$
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$ and any natural number $p$, the expansion of $f$ by a factor of $p$ is equal to the composition of $f$ with the monomial $X^p$, i.e., \[ \text{expand}_R p f = f \circ (X^p). \]
Polynomial.expand_eq_sum theorem
{f : R[X]} : expand R p f = f.sum fun e a => C a * (X ^ p) ^ e
Full source 
theorem expand_eq_sum {f : R[X]} : expand R p f = f.sum fun e a => C a * (X ^ p) ^ e := by
  simp [expand, eval₂]
Expansion of Polynomial as Sum of Scaled Powers
Informal description
For any polynomial $f = \sum_{n} a_n X^n$ over a commutative semiring $R$ and any natural number $p$, the expansion of $f$ by a factor of $p$ is given by $\text{expand}_R p f = \sum_{n} a_n X^{n p}$.
Polynomial.expand_C theorem
(r : R) : expand R p (C r) = C r
Full source 
@[simp]
theorem expand_C (r : R) : expand R p (C r) = C r :=
  eval₂_C _ _
Expansion Preserves Constant Polynomials: $\text{expand}_R p (C(r)) = C(r)$
Informal description
For any commutative semiring $R$, natural number $p$, and element $r \in R$, the expansion of the constant polynomial $C(r)$ by a factor of $p$ is equal to $C(r)$ itself, i.e., $\text{expand}_R p (C(r)) = C(r)$.
Polynomial.expand_X theorem
: expand R p X = X ^ p
Full source 
@[simp]
theorem expand_X : expand R p X = X ^ p :=
  eval₂_X _ _
Expansion of Polynomial Variable: $\text{expand}_R p (X) = X^p$
Informal description
For a commutative semiring $R$ and a natural number $p$, the expansion of the polynomial variable $X$ by a factor of $p$ is equal to $X$ raised to the power $p$, i.e., $\text{expand}_R p (X) = X^p$.
Polynomial.expand_monomial theorem
(r : R) : expand R p (monomial q r) = monomial (q * p) r
Full source 
@[simp]
theorem expand_monomial (r : R) : expand R p (monomial q r) = monomial (q * p) r := by
  simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]
Expansion of Monomial: $\text{expand}_R p (rX^q) = rX^{q p}$
Informal description
For any commutative semiring $R$, natural numbers $p$ and $q$, and element $r \in R$, the expansion of the monomial $rX^q$ by a factor of $p$ is equal to the monomial $rX^{q \cdot p}$, i.e., \[ \text{expand}_R p (rX^q) = rX^{q \cdot p}. \]
Polynomial.expand_expand theorem
(f : R[X]) : expand R p (expand R q f) = expand R (p * q) f
Full source 
theorem expand_expand (f : R[X]) : expand R p (expand R q f) = expand R (p * q) f :=
  Polynomial.induction_on f (fun r => by simp_rw [expand_C])
    (fun f g ihf ihg => by simp_rw [map_add, ihf, ihg]) fun n r _ => by
    simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]
Composition of Polynomial Expansions: $\text{expand}_R\, p \circ \text{expand}_R\, q = \text{expand}_R\, (p \cdot q)$
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$ and natural numbers $p, q$, the expansion of $f$ by a factor of $p$ followed by expansion by a factor of $q$ is equal to expanding $f$ by a factor of $p \cdot q$, i.e., \[ \text{expand}_R\, p\, (\text{expand}_R\, q\, f) = \text{expand}_R\, (p \cdot q)\, f. \]
Polynomial.expand_mul theorem
(f : R[X]) : expand R (p * q) f = expand R p (expand R q f)
Full source 
theorem expand_mul (f : R[X]) : expand R (p * q) f = expand R p (expand R q f) :=
  (expand_expand p q f).symm
Composition of Polynomial Expansions: $\text{expand}_R (p \cdot q) = \text{expand}_R p \circ \text{expand}_R q$
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$ and natural numbers $p, q$, the expansion of $f$ by a factor of $p \cdot q$ is equal to expanding $f$ by a factor of $q$ followed by expansion by a factor of $p$, i.e., \[ \text{expand}_R (p \cdot q) f = \text{expand}_R p (\text{expand}_R q f). \]
Polynomial.expand_zero theorem
(f : R[X]) : expand R 0 f = C (eval 1 f)
Full source 
@[simp]
theorem expand_zero (f : R[X]) : expand R 0 f = C (eval 1 f) := by simp [expand]
Expansion by Zero Factor Yields Constant Polynomial of Evaluation at One
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$, the expansion of $f$ by a factor of $0$ is equal to the constant polynomial whose coefficient is the evaluation of $f$ at $1$, i.e., \[ \text{expand}_R\, 0\, f = C(f(1)). \]
Polynomial.expand_one theorem
(f : R[X]) : expand R 1 f = f
Full source 
@[simp]
theorem expand_one (f : R[X]) : expand R 1 f = f :=
  Polynomial.induction_on f (fun r => by rw [expand_C])
    (fun f g ihf ihg => by rw [map_add, ihf, ihg]) fun n r _ => by
    rw [map_mul, expand_C, map_pow, expand_X, pow_one]
Identity Expansion of Polynomials: $\text{expand}_R\, 1\, f = f$
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$, the expansion of $f$ by a factor of 1 is equal to $f$ itself, i.e., $\text{expand}_R\, 1\, f = f$.
Polynomial.expand_pow theorem
(f : R[X]) : expand R (p ^ q) f = (expand R p)^[q] f
Full source 
theorem expand_pow (f : R[X]) : expand R (p ^ q) f = (expand R p)^[q] f :=
  Nat.recOn q (by rw [pow_zero, expand_one, Function.iterate_zero, id]) fun n ih => by
    rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]
Iterated Polynomial Expansion: $\text{expand}_R (p^q) = (\text{expand}_R p)^q$
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$ and natural numbers $p, q$, the expansion of $f$ by a factor of $p^q$ is equal to the $q$-th iterate of the expansion map by $p$ applied to $f$, i.e., \[ \text{expand}_R (p^q) f = (\text{expand}_R p)^{[q]} f. \]
Polynomial.derivative_expand theorem
(f : R[X]) : Polynomial.derivative (expand R p f) = expand R p (Polynomial.derivative f) * (p * (X ^ (p - 1) : R[X]))
Full source 
theorem derivative_expand (f : R[X]) : Polynomial.derivative (expand R p f) =
    expand R p (Polynomial.derivative f) * (p * (X ^ (p - 1) : R[X])) := by
  rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]
Derivative of Expanded Polynomial: $\frac{d}{dX} (\text{expand}_p f) = \text{expand}_p (f') \cdot p X^{p-1}$
Informal description
For any polynomial $f \in R[X]$ over a commutative semiring $R$, the derivative of the expanded polynomial $\text{expand}_R p(f)$ is equal to the expansion of the derivative of $f$ multiplied by $p X^{p-1}$. That is, \[ \frac{d}{dX} \left( \sum a_n X^{n p} \right) = \left( \sum \frac{d a_n}{dX} X^{n p} \right) \cdot p X^{p-1}. \]
Polynomial.coeff_expand theorem
{p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : (expand R p f).coeff n = if p ∣ n then f.coeff (n / p) else 0
Full source 
theorem coeff_expand {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
    (expand R p f).coeff n = if p ∣ n then f.coeff (n / p) else 0 := by
  simp only [expand_eq_sum]
  simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]
  split_ifs with h
  · rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
    · intro b _ hb2
      rw [if_neg]
      intro hb3
      apply hb2
      rw [← hb3, Nat.mul_div_cancel_left b hp]
    · intro hn
      rw [not_mem_support_iff.1 hn]
      split_ifs <;> rfl
  · rw [Finset.sum_eq_zero]
    intro k _
    rw [if_neg]
    exact fun hkn => h ⟨k, hkn.symm⟩
Coefficient Formula for Expanded Polynomial: $(\text{expand}_R p f)_n = a_{n/p} \cdot \mathbf{1}_{p \mid n}$
Informal description
Let $R$ be a commutative semiring and $p$ a positive natural number. For any polynomial $f = \sum_{k} a_k X^k \in R[X]$ and any natural number $n$, the coefficient of $X^n$ in the expanded polynomial $\text{expand}_R p f$ is given by: \[ (\text{expand}_R p f)_n = \begin{cases} a_{n/p} & \text{if } p \text{ divides } n, \\ 0 & \text{otherwise.} \end{cases} \]
Polynomial.coeff_expand_mul theorem
{p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : (expand R p f).coeff (n * p) = f.coeff n
Full source 
@[simp]
theorem coeff_expand_mul {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
    (expand R p f).coeff (n * p) = f.coeff n := by
  rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]
Coefficient of Expanded Polynomial at Multiple Index: $(\text{expand}_R p f)_{n p} = a_n$
Informal description
Let $R$ be a commutative semiring and $p$ a positive natural number. For any polynomial $f = \sum_{k} a_k X^k \in R[X]$ and any natural number $n$, the coefficient of $X^{n p}$ in the expanded polynomial $\text{expand}_R p f$ is equal to the coefficient of $X^n$ in $f$, i.e., \[ (\text{expand}_R p f)_{n p} = a_n. \]
Polynomial.coeff_expand_mul' theorem
{p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) : (expand R p f).coeff (p * n) = f.coeff n
Full source 
@[simp]
theorem coeff_expand_mul' {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
    (expand R p f).coeff (p * n) = f.coeff n := by rw [mul_comm, coeff_expand_mul hp]
Coefficient of Expanded Polynomial at Scaled Index: $(\text{expand}_R p f)_{p n} = a_n$
Informal description
Let $R$ be a commutative semiring and $p$ a positive natural number. For any polynomial $f = \sum_{k} a_k X^k \in R[X]$ and any natural number $n$, the coefficient of $X^{p n}$ in the expanded polynomial $\text{expand}_R p f$ is equal to the coefficient of $X^n$ in $f$, i.e., \[ (\text{expand}_R p f)_{p n} = a_n. \]
Polynomial.expand_injective theorem
{n : ℕ} (hn : 0 < n) : Function.Injective (expand R n)
Full source 
/-- Expansion is injective. -/
theorem expand_injective {n : ℕ} (hn : 0 < n) : Function.Injective (expand R n) := fun g g' H =>
  ext fun k => by rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]
Injectivity of Polynomial Expansion: $\text{expand}_R n$ is Injective for $n > 0$
Informal description
For any positive natural number $n$, the polynomial expansion map $\text{expand}_R n : R[X] \to R[X]$, which sends a polynomial $\sum a_k X^k$ to $\sum a_k X^{n k}$, is injective. In other words, if $\text{expand}_R n f = \text{expand}_R n g$ for polynomials $f, g \in R[X]$, then $f = g$.
Polynomial.expand_inj theorem
{p : ℕ} (hp : 0 < p) {f g : R[X]} : expand R p f = expand R p g ↔ f = g
Full source 
theorem expand_inj {p : ℕ} (hp : 0 < p) {f g : R[X]} : expandexpand R p f = expand R p g ↔ f = g :=
  (expand_injective hp).eq_iff
Expansion of Polynomials is Injective for Positive $p$
Informal description
For any positive natural number $p$ and polynomials $f, g \in R[X]$, the expansion $\text{expand}_R p f$ is equal to $\text{expand}_R p g$ if and only if $f = g$.
Polynomial.expand_eq_zero theorem
{p : ℕ} (hp : 0 < p) {f : R[X]} : expand R p f = 0 ↔ f = 0
Full source 
theorem expand_eq_zero {p : ℕ} (hp : 0 < p) {f : R[X]} : expandexpand R p f = 0 ↔ f = 0 :=
  (expand_injective hp).eq_iff' (map_zero _)
Zero Polynomial Characterization under Expansion: $\text{expand}_R p f = 0 \leftrightarrow f = 0$
Informal description
For any positive natural number $p$ and any polynomial $f \in R[X]$, the expansion of $f$ by a factor of $p$ is the zero polynomial if and only if $f$ is the zero polynomial. In other words, $\text{expand}_R p f = 0 \leftrightarrow f = 0$.
Polynomial.expand_ne_zero theorem
{p : ℕ} (hp : 0 < p) {f : R[X]} : expand R p f ≠ 0 ↔ f ≠ 0
Full source 
theorem expand_ne_zero {p : ℕ} (hp : 0 < p) {f : R[X]} : expandexpand R p f ≠ 0expand R p f ≠ 0 ↔ f ≠ 0 :=
  (expand_eq_zero hp).not
Nonzero Polynomial Characterization under Expansion: $\text{expand}_R p f \neq 0 \leftrightarrow f \neq 0$
Informal description
For any positive natural number $p$ and any polynomial $f \in R[X]$, the expansion $\text{expand}_R p f$ is nonzero if and only if $f$ is nonzero. In other words, $\text{expand}_R p f \neq 0 \leftrightarrow f \neq 0$.
Polynomial.expand_eq_C theorem
{p : ℕ} (hp : 0 < p) {f : R[X]} {r : R} : expand R p f = C r ↔ f = C r
Full source 
theorem expand_eq_C {p : ℕ} (hp : 0 < p) {f : R[X]} {r : R} : expandexpand R p f = C r ↔ f = C r := by
  rw [← expand_C, expand_inj hp, expand_C]
Expansion of Polynomial Equals Constant Polynomial if and only if Original Polynomial is Constant: $\text{expand}_R p f = C(r) \leftrightarrow f = C(r)$
Informal description
For any positive natural number $p$, polynomial $f \in R[X]$, and element $r \in R$, the expansion $\text{expand}_R p f$ equals the constant polynomial $C(r)$ if and only if $f$ equals $C(r)$. In other words, $\text{expand}_R p f = C(r) \leftrightarrow f = C(r)$.
Polynomial.natDegree_expand theorem
(p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.natDegree * p
Full source 
theorem natDegree_expand (p : ℕ) (f : R[X]) : (expand R p f).natDegree = f.natDegree * p := by
  rcases p.eq_zero_or_pos with hp | hp
  · rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
  by_cases hf : f = 0
  · rw [hf, map_zero, natDegree_zero, zero_mul]
  have hf1 : expandexpand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hf1]
  refine le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => ?_) ?_
  · rw [coeff_expand hp]
    split_ifs with hpn
    · rw [coeff_eq_zero_of_natDegree_lt]
      contrapose! hn
      norm_cast
      rw [← Nat.div_mul_cancel hpn]
      exact Nat.mul_le_mul_right p hn
    · rfl
  · refine le_degree_of_ne_zero ?_
    rw [coeff_expand_mul hp, ← leadingCoeff]
    exact mt leadingCoeff_eq_zero.1 hf
Degree of Expanded Polynomial: $\deg(\text{expand}_R p f) = \deg(f) \cdot p$
Informal description
For any natural number $p$ and any polynomial $f \in R[X]$, the natural degree of the expanded polynomial $\text{expand}_R p f$ is equal to the natural degree of $f$ multiplied by $p$, i.e., $\deg(\text{expand}_R p f) = \deg(f) \cdot p$.
Polynomial.leadingCoeff_expand theorem
{p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).leadingCoeff = f.leadingCoeff
Full source 
theorem leadingCoeff_expand {p : ℕ} {f : R[X]} (hp : 0 < p) :
    (expand R p f).leadingCoeff = f.leadingCoeff := by
  simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]
Leading Coefficient Preservation under Polynomial Expansion: $(\text{expand}_R p f)_{\text{lead}} = f_{\text{lead}}$
Informal description
For any positive natural number $p$ and any polynomial $f \in R[X]$, the leading coefficient of the expanded polynomial $\text{expand}_R p f$ is equal to the leading coefficient of $f$.
Polynomial.monic_expand_iff theorem
{p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).Monic ↔ f.Monic
Full source 
theorem monic_expand_iff {p : ℕ} {f : R[X]} (hp : 0 < p) : (expand R p f).Monic ↔ f.Monic := by
  simp only [Monic, leadingCoeff_expand hp]
Monicity Preservation under Polynomial Expansion: $\text{expand}_R p f$ monic $\iff$ $f$ monic
Informal description
For any positive natural number $p$ and any polynomial $f \in R[X]$, the expanded polynomial $\text{expand}_R p f$ is monic if and only if $f$ is monic.
Polynomial.map_expand theorem
{p : ℕ} {f : R →+* S} {q : R[X]} : map f (expand R p q) = expand S p (map f q)
Full source 
theorem map_expand {p : ℕ} {f : R →+* S} {q : R[X]} :
    map f (expand R p q) = expand S p (map f q) := by
  by_cases hp : p = 0
  · simp [hp]
  ext
  rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
  split_ifs <;> simp_all
Compatibility of Polynomial Expansion with Ring Homomorphism: $f_* \circ \text{expand}_R p = \text{expand}_S p \circ f_*$
Informal description
Let $R$ and $S$ be commutative semirings, $p$ a natural number, and $f : R \to S$ a ring homomorphism. For any polynomial $q \in R[X]$, the following equality holds: \[ f_*(\text{expand}_R p\, q) = \text{expand}_S p\, (f_* q) \] where $f_*$ denotes the polynomial map induced by $f$, and $\text{expand}_R p$ is the expansion operation that sends $\sum a_n X^n$ to $\sum a_n X^{n p}$.
Polynomial.expand_eval theorem
(p : ℕ) (P : R[X]) (r : R) : eval r (expand R p P) = eval (r ^ p) P
Full source 
@[simp]
theorem expand_eval (p : ℕ) (P : R[X]) (r : R) : eval r (expand R p P) = eval (r ^ p) P := by
  refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
  rw [map_add, eval_add, eval_add, hf, hg]
Evaluation of Expanded Polynomial: $\text{eval}(r, \text{expand}_R p (P)) = \text{eval}(r^p, P)$
Informal description
For any natural number $p$, polynomial $P \in R[X]$, and element $r \in R$, evaluating the expanded polynomial $\text{expand}_R p (P)$ at $r$ is equal to evaluating $P$ at $r^p$, i.e., \[ \text{eval}(r, \text{expand}_R p (P)) = \text{eval}(r^p, P). \]
Polynomial.expand_aeval theorem
{A : Type*} [Semiring A] [Algebra R A] (p : ℕ) (P : R[X]) (r : A) : aeval r (expand R p P) = aeval (r ^ p) P
Full source 
@[simp]
theorem expand_aeval {A : Type*} [Semiring A] [Algebra R A] (p : ℕ) (P : R[X]) (r : A) :
    aeval r (expand R p P) = aeval (r ^ p) P := by
  refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp
  rw [map_add, aeval_add, aeval_add, hf, hg]
Evaluation of Expanded Polynomial: $\text{aeval}_r(\text{expand}_R p P) = \text{aeval}_{r^p}(P)$
Informal description
Let $R$ be a commutative semiring, $A$ a semiring with an $R$-algebra structure, $p$ a natural number, $P \in R[X]$ a polynomial, and $r \in A$ an element. Then the evaluation of the expanded polynomial $\text{expand}_R p P$ at $r$ equals the evaluation of $P$ at $r^p$, i.e., \[ \text{aeval}_r(\text{expand}_R p P) = \text{aeval}_{r^p}(P). \]
Polynomial.contract definition
(p : ℕ) (f : R[X]) : R[X]
Full source 
/-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. -/
noncomputable def contract (p : ℕ) (f : R[X]) : R[X] :=
  ∑ n ∈ range (f.natDegree + 1), monomial n (f.coeff (n * p))
Polynomial contraction by \( p \)
Informal description
Given a natural number \( p \) and a polynomial \( f(X) = \sum_{n} a_n X^n \) over a commutative semiring \( R \), the contraction of \( f \) by \( p \) is the polynomial \( \sum_{n} a_{n p} X^n \). This operation is the inverse of polynomial expansion, which sends \( \sum_{n} a_n X^n \) to \( \sum_{n} a_n X^{n p} \).
Polynomial.coeff_contract theorem
{p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) : (contract p f).coeff n = f.coeff (n * p)
Full source 
theorem coeff_contract {p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) :
    (contract p f).coeff n = f.coeff (n * p) := by
  simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt,
    ite_eq_left_iff]
  intro hn
  apply (coeff_eq_zero_of_natDegree_lt _).symm
  calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)
Coefficient formula for polynomial contraction: $\text{coeff}(\mathrm{contract}_p(f), n) = \text{coeff}(f, n p)$
Informal description
Let $R$ be a commutative semiring, $p$ a nonzero natural number, and $f(X) = \sum_{k} a_k X^k$ a polynomial in $R[X]$. Then the coefficient of $X^n$ in the contracted polynomial $\mathrm{contract}_p(f)$ is equal to the coefficient of $X^{n p}$ in $f$, i.e., \[ \text{coeff}(\mathrm{contract}_p(f), n) = \text{coeff}(f, n p). \]
Polynomial.map_contract theorem
{p : ℕ} (hp : p ≠ 0) {f : R →+* S} {q : R[X]} : (q.contract p).map f = (q.map f).contract p
Full source 
theorem map_contract {p : ℕ} (hp : p ≠ 0) {f : R →+* S} {q : R[X]} :
    (q.contract p).map f = (q.map f).contract p := ext fun n ↦ by
  simp only [coeff_map, coeff_contract hp]
Commutativity of Polynomial Contraction with Ring Homomorphism Application: $f(\mathrm{contract}_p(q)) = \mathrm{contract}_p(f(q))$
Informal description
Let $R$ and $S$ be commutative semirings, $p$ a nonzero natural number, and $f : R \to S$ a ring homomorphism. For any polynomial $q \in R[X]$, the image under $f$ of the contracted polynomial $\mathrm{contract}_p(q)$ is equal to the contraction of the image of $q$ under $f$, i.e., \[ f(\mathrm{contract}_p(q)) = \mathrm{contract}_p(f(q)). \]
Polynomial.contract_expand theorem
{f : R[X]} (hp : p ≠ 0) : contract p (expand R p f) = f
Full source 
theorem contract_expand {f : R[X]} (hp : p ≠ 0) : contract p (expand R p f) = f := by
  ext
  simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]
Inverse Property of Polynomial Expansion and Contraction: $\mathrm{contract}_p \circ \mathrm{expand}_R p = \mathrm{id}$
Informal description
Let $R$ be a commutative semiring and $p$ a nonzero natural number. For any polynomial $f \in R[X]$, the contraction of the expansion of $f$ by $p$ equals $f$ itself, i.e., \[ \mathrm{contract}_p(\mathrm{expand}_R p f) = f. \]
Polynomial.contract_one theorem
{f : R[X]} : contract 1 f = f
Full source 
theorem contract_one {f : R[X]} : contract 1 f = f :=
  ext fun n ↦ by rw [coeff_contract one_ne_zero, mul_one]
Identity Property of Polynomial Contraction: $\mathrm{contract}_1(f) = f$
Informal description
For any polynomial $f$ with coefficients in a commutative semiring $R$, the contraction of $f$ by $1$ is equal to $f$ itself, i.e., $\mathrm{contract}_1(f) = f$.
Polynomial.contract_C theorem
(r : R) : contract p (C r) = C r
Full source 
@[simp] theorem contract_C (r : R) : contract p (C r) = C r := by simp [contract]
Contraction Preserves Constant Polynomials: $\text{contract}_p(C(r)) = C(r)$
Informal description
For any element $r$ in a commutative semiring $R$ and any natural number $p$, the contraction of the constant polynomial $C(r)$ by $p$ is equal to $C(r)$ itself.
Polynomial.contract_add theorem
{p : ℕ} (hp : p ≠ 0) (f g : R[X]) : contract p (f + g) = contract p f + contract p g
Full source 
theorem contract_add {p : ℕ} (hp : p ≠ 0) (f g : R[X]) :
    contract p (f + g) = contract p f + contract p g := by
  ext; simp_rw [coeff_add, coeff_contract hp, coeff_add]
Additivity of Polynomial Contraction: $\mathrm{contract}_p(f + g) = \mathrm{contract}_p(f) + \mathrm{contract}_p(g)$
Informal description
Let $R$ be a commutative semiring, $p$ a nonzero natural number, and $f, g \in R[X]$ polynomials. Then the contraction of the sum $f + g$ by $p$ equals the sum of the contractions of $f$ and $g$ by $p$, i.e., \[ \mathrm{contract}_p(f + g) = \mathrm{contract}_p(f) + \mathrm{contract}_p(g). \]
Polynomial.contract_mul_expand theorem
{p : ℕ} (hp : p ≠ 0) (f g : R[X]) : contract p (f * expand R p g) = contract p f * g
Full source 
theorem contract_mul_expand {p : ℕ} (hp : p ≠ 0) (f g : R[X]) :
    contract p (f * expand R p g) = contract p f * g := by
  ext n
  rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]
  · simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]
  · intro x hx y hy eq; simpa only [Prod.ext_iff, Nat.mul_right_cancel_iff hp.bot_lt] using eq
  · simp_rw [subset_iff, mem_image, mem_antidiagonal]; rintro _ ⟨x, rfl, rfl⟩; simp_rw [add_mul]
  simp_rw [mem_image, mem_antidiagonal]
  intro ⟨x, y⟩ eq nex
  by_cases h : p ∣ y
  · obtain ⟨x, rfl⟩ : p ∣ x := (Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)
    obtain ⟨y, rfl⟩ := h
    refine (nex ⟨⟨x, y⟩, (Nat.mul_right_cancel_iff hp.bot_lt).mp ?_, by simp_rw [mul_comm]⟩).elim
    rw [← eq, mul_comm, mul_add]
  · rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]
Contraction-Expansion Product Identity: $\text{contract}_p(f \cdot \text{expand}_R p g) = (\text{contract}_p f) \cdot g$
Informal description
Let $R$ be a commutative semiring and $p$ a nonzero natural number. For any polynomials $f, g \in R[X]$, the contraction of the product $f \cdot \text{expand}_R p g$ by $p$ equals the product of the contraction of $f$ by $p$ and $g$, i.e., \[ \text{contract}_p(f \cdot \text{expand}_R p g) = (\text{contract}_p f) \cdot g. \]
Polynomial.isCoprime_expand theorem
{f g : R[X]} {p : ℕ} (hp : p ≠ 0) : IsCoprime (expand R p f) (expand R p g) ↔ IsCoprime f g
Full source 
@[simp] theorem isCoprime_expand {f g : R[X]} {p : ℕ} (hp : p ≠ 0) :
    IsCoprimeIsCoprime (expand R p f) (expand R p g) ↔ IsCoprime f g :=
  ⟨fun ⟨a, b, eq⟩ ↦ ⟨contract p a, contract p b, by
    simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]⟩, (·.map _)⟩
Coprimality is preserved under polynomial expansion: $\text{IsCoprime}(\text{expand}_R p f, \text{expand}_R p g) \leftrightarrow \text{IsCoprime}(f, g)$
Informal description
Let $R$ be a commutative semiring, $f, g \in R[X]$ polynomials, and $p$ a nonzero natural number. Then the expanded polynomials $\text{expand}_R p f$ and $\text{expand}_R p g$ are coprime if and only if $f$ and $g$ are coprime.
Polynomial.expand_contract theorem
[CharP R p] [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) (hp : p ≠ 0) : expand R p (contract p f) = f
Full source 
theorem expand_contract [CharP R p] [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0)
    (hp : p ≠ 0) : expand R p (contract p f) = f := by
  ext n
  rw [coeff_expand hp.bot_lt, coeff_contract hp]
  split_ifs with h
  · rw [Nat.div_mul_cancel h]
  · rcases n with - | n
    · exact absurd (dvd_zero p) h
    have := coeff_derivative f n
    rw [hf, coeff_zero, zero_eq_mul] at this
    rcases this with h' | _
    · rw [h']
    rename_i _ _ _ h'
    rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'
    exact absurd h' h
Expansion-Contraction Identity for Polynomials in Characteristic $p$: $\text{expand}_R p \circ \text{contract}_p = \text{id}$ on Derivative-Zero Polynomials
Informal description
Let $R$ be a commutative semiring of characteristic $p$ with no zero divisors, and let $f \in R[X]$ be a polynomial with zero derivative. Then for any nonzero natural number $p$, the expansion of the contraction of $f$ by $p$ equals $f$, i.e., \[ \text{expand}_R p (\text{contract}_p f) = f. \]
Polynomial.expand_contract' theorem
[NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) : expand R p (contract p f) = f
Full source 
theorem expand_contract' [NoZeroDivisors R] {f : R[X]} (hf : Polynomial.derivative f = 0) :
    expand R p (contract p f) = f := by
  obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›
  · rw [expand_one, contract_one]
  · haveI := Fact.mk hchar; exact expand_contract p hf hprime.ne_zero
Expansion-Contraction Identity for Derivative-Zero Polynomials: $\text{expand}_R p \circ \text{contract}_p = \text{id}$
Informal description
Let $R$ be a commutative semiring with no zero divisors, and let $f \in R[X]$ be a polynomial with zero derivative. Then the expansion of the contraction of $f$ by $p$ equals $f$, i.e., \[ \text{expand}_R p (\text{contract}_p f) = f. \]
Polynomial.expand_char theorem
(f : R[X]) : map (frobenius R p) (expand R p f) = f ^ p
Full source 
theorem expand_char (f : R[X]) : map (frobenius R p) (expand R p f) = f ^ p := by
  refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_
  · rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]
  · rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
      mul_pow, ← C.map_pow, frobenius_def]
    ring
Frobenius-Expansion Identity: $\text{Frob}_p(\text{expand}_R p f) = f^p$
Informal description
Let $R$ be a commutative semiring of exponential characteristic $p$ and let $f \in R[X]$ be a polynomial. Then applying the Frobenius endomorphism to the expansion of $f$ by $p$ yields the $p$-th power of $f$, i.e., \[ \text{Frob}_p(\text{expand}_R p f) = f^p. \]
Polynomial.map_expand_pow_char theorem
(f : R[X]) (n : ℕ) : map (frobenius R p ^ n) (expand R (p ^ n) f) = f ^ p ^ n
Full source 
theorem map_expand_pow_char (f : R[X]) (n : ℕ) :
    map (frobenius R p ^ n) (expand R (p ^ n) f) = f ^ p ^ n := by
  induction n with
  | zero => simp [RingHom.one_def]
  | succ _ n_ih =>
    symm
    rw [pow_succ, pow_mul, ← n_ih, ← expand_char, pow_succ', RingHom.mul_def, ← map_map, mul_comm,
      expand_mul, ← map_expand]
Frobenius-Expansion-Power Identity: $\text{Frob}_p^n(\text{expand}_R (p^n) f) = f^{p^n}$
Informal description
Let $R$ be a commutative semiring of exponential characteristic $p$, and let $f \in R[X]$ be a polynomial. For any natural number $n$, applying the $n$-th iterate of the Frobenius endomorphism to the expansion of $f$ by $p^n$ yields the $p^n$-th power of $f$, i.e., \[ \text{Frob}_p^n(\text{expand}_R (p^n) f) = f^{p^n}. \]
Polynomial.rootMultiplicity_expand_pow theorem
: (expand R (p ^ n) f).rootMultiplicity r = p ^ n * f.rootMultiplicity (r ^ p ^ n)
Full source 
theorem rootMultiplicity_expand_pow :
    (expand R (p ^ n) f).rootMultiplicity r = p ^ n * f.rootMultiplicity (r ^ p ^ n) := by
  obtain rfl | h0 := eq_or_ne f 0; · simp
  obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)
  rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd
  conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]
Root Multiplicity under $p^n$-th Power Expansion: $\text{rootMultiplicity}(r, \text{expand}_R (p^n) f) = p^n \cdot \text{rootMultiplicity}(r^{p^n}, f)$
Informal description
Let $R$ be a commutative semiring of exponential characteristic $p$, $f \in R[X]$ a polynomial, $r \in R$ an element, and $n \in \mathbb{N}$ a natural number. Then the root multiplicity of $r$ in the polynomial $\text{expand}_R (p^n) f$ is equal to $p^n$ times the root multiplicity of $r^{p^n}$ in $f$, i.e., \[ \text{rootMultiplicity}(r, \text{expand}_R (p^n) f) = p^n \cdot \text{rootMultiplicity}(r^{p^n}, f). \]
Polynomial.rootMultiplicity_expand theorem
: (expand R p f).rootMultiplicity r = p * f.rootMultiplicity (r ^ p)
Full source 
theorem rootMultiplicity_expand :
    (expand R p f).rootMultiplicity r = p * f.rootMultiplicity (r ^ p) := by
  rw [← pow_one p, rootMultiplicity_expand_pow]
Root Multiplicity under $p$-th Power Expansion: $\text{rootMultiplicity}(r, \text{expand}_R p f) = p \cdot \text{rootMultiplicity}(r^p, f)$
Informal description
Let $R$ be a commutative semiring of exponential characteristic $p$, $f \in R[X]$ a polynomial, and $r \in R$ an element. Then the root multiplicity of $r$ in the polynomial $\text{expand}_R p f$ is equal to $p$ times the root multiplicity of $r^p$ in $f$, i.e., \[ \text{rootMultiplicity}(r, \text{expand}_R p f) = p \cdot \text{rootMultiplicity}(r^p, f). \]
Polynomial.isLocalHom_expand theorem
{p : ℕ} (hp : 0 < p) : IsLocalHom (expand R p)
Full source 
theorem isLocalHom_expand {p : ℕ} (hp : 0 < p) : IsLocalHom (expand R p) := by
  refine ⟨fun f hf1 => ?_⟩
  have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
  rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
  rw [hf2, isUnit_C] at hf1; rw [expand_eq_C hp] at hf2; rwa [hf2, isUnit_C]
Polynomial Expansion is a Local Homomorphism for Positive $p$
Informal description
For any positive natural number $p$, the polynomial expansion map $\text{expand}_R p : R[X] \to R[X]$ is a local homomorphism. That is, for any polynomial $f \in R[X]$, if $\text{expand}_R p f$ is a unit in $R[X]$, then $f$ is a unit in $R[X]$.
Polynomial.of_irreducible_expand theorem
{p : ℕ} (hp : p ≠ 0) {f : R[X]} (hf : Irreducible (expand R p f)) : Irreducible f
Full source 
theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : R[X]} (hf : Irreducible (expand R p f)) :
    Irreducible f :=
  let _ := isLocalHom_expand R hp.bot_lt
  hf.of_map
Irreducibility of Polynomial Implies Irreducibility of Its Expansion
Informal description
Let $R$ be a commutative semiring and $p$ a nonzero natural number. For any polynomial $f \in R[X]$, if the expanded polynomial $\text{expand}_R p f$ is irreducible, then $f$ is irreducible.
Polynomial.of_irreducible_expand_pow theorem
{p : ℕ} (hp : p ≠ 0) {f : R[X]} {n : ℕ} : Irreducible (expand R (p ^ n) f) → Irreducible f
Full source 
theorem of_irreducible_expand_pow {p : ℕ} (hp : p ≠ 0) {f : R[X]} {n : ℕ} :
    Irreducible (expand R (p ^ n) f) → Irreducible f :=
  Nat.recOn n (fun hf => by rwa [pow_zero, expand_one] at hf) fun n ih hf =>
    ih <| of_irreducible_expand hp <| by
      rw [pow_succ'] at hf
      rwa [expand_expand]
Irreducibility of Polynomial Implies Irreducibility of Its $p^n$-th Expansion
Informal description
Let $R$ be a commutative semiring and $p$ a nonzero natural number. For any polynomial $f \in R[X]$ and natural number $n$, if the expanded polynomial $\text{expand}_R (p^n) f$ is irreducible, then $f$ is irreducible.