Expand a polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
polynomial.expand R p f: expand the polynomialfwith coefficients in a commutative semiringRby a factor of p, soexpand R p (∑ aₙ xⁿ)is∑ aₙ xⁿᵖ.polynomial.contract p f: the opposite ofexpand, so it sends∑ aₙ xⁿᵖto∑ aₙ xⁿ.
noncomputable
def
polynomial.expand
(R : Type u)
[comm_semiring R]
(p : ℕ) :
polynomial R →ₐ[R] polynomial R
Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.
Equations
- polynomial.expand R p = {to_fun := (polynomial.eval₂_ring_hom polynomial.C (polynomial.X ^ p)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
polynomial.coe_expand
(R : Type u)
[comm_semiring R]
(p : ℕ) :
⇑(polynomial.expand R p) = polynomial.eval₂ polynomial.C (polynomial.X ^ p)
theorem
polynomial.expand_eq_sum
{R : Type u}
[comm_semiring R]
(p : ℕ)
{f : polynomial R} :
⇑(polynomial.expand R p) f = f.sum (λ (e : ℕ) (a : R), ⇑polynomial.C a * (polynomial.X ^ p) ^ e)
@[simp]
theorem
polynomial.expand_C
{R : Type u}
[comm_semiring R]
(p : ℕ)
(r : R) :
⇑(polynomial.expand R p) (⇑polynomial.C r) = ⇑polynomial.C r
@[simp]
theorem
polynomial.expand_X
{R : Type u}
[comm_semiring R]
(p : ℕ) :
⇑(polynomial.expand R p) polynomial.X = polynomial.X ^ p
@[simp]
theorem
polynomial.expand_monomial
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(r : R) :
⇑(polynomial.expand R p) (⇑(polynomial.monomial q) r) = ⇑(polynomial.monomial (q * p)) r
theorem
polynomial.expand_expand
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(f : polynomial R) :
⇑(polynomial.expand R p) (⇑(polynomial.expand R q) f) = ⇑(polynomial.expand R (p * q)) f
theorem
polynomial.expand_mul
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(f : polynomial R) :
⇑(polynomial.expand R (p * q)) f = ⇑(polynomial.expand R p) (⇑(polynomial.expand R q) f)
@[simp]
theorem
polynomial.expand_zero
{R : Type u}
[comm_semiring R]
(f : polynomial R) :
⇑(polynomial.expand R 0) f = ⇑polynomial.C (polynomial.eval 1 f)
@[simp]
theorem
polynomial.expand_one
{R : Type u}
[comm_semiring R]
(f : polynomial R) :
⇑(polynomial.expand R 1) f = f
theorem
polynomial.expand_pow
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(f : polynomial R) :
⇑(polynomial.expand R (p ^ q)) f = ⇑(polynomial.expand R p)^[q] f
theorem
polynomial.derivative_expand
{R : Type u}
[comm_semiring R]
(p : ℕ)
(f : polynomial R) :
⇑polynomial.derivative (⇑(polynomial.expand R p) f) = ⇑(polynomial.expand R p) (⇑polynomial.derivative f) * (↑p * polynomial.X ^ (p - 1))
theorem
polynomial.coeff_expand
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
(f : polynomial R)
(n : ℕ) :
@[simp]
theorem
polynomial.coeff_expand_mul
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
(f : polynomial R)
(n : ℕ) :
@[simp]
theorem
polynomial.coeff_expand_mul'
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
(f : polynomial R)
(n : ℕ) :
Expansion is injective.
theorem
polynomial.expand_inj
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
{f g : polynomial R} :
⇑(polynomial.expand R p) f = ⇑(polynomial.expand R p) g ↔ f = g
theorem
polynomial.expand_eq_zero
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
{f : polynomial R} :
⇑(polynomial.expand R p) f = 0 ↔ f = 0
theorem
polynomial.expand_ne_zero
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
{f : polynomial R} :
⇑(polynomial.expand R p) f ≠ 0 ↔ f ≠ 0
theorem
polynomial.expand_eq_C
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
{f : polynomial R}
{r : R} :
⇑(polynomial.expand R p) f = ⇑polynomial.C r ↔ f = ⇑polynomial.C r
theorem
polynomial.nat_degree_expand
{R : Type u}
[comm_semiring R]
(p : ℕ)
(f : polynomial R) :
(⇑(polynomial.expand R p) f).nat_degree = f.nat_degree * p
theorem
polynomial.monic.expand
{R : Type u}
[comm_semiring R]
{p : ℕ}
{f : polynomial R}
(hp : 0 < p)
(h : f.monic) :
(⇑(polynomial.expand R p) f).monic
theorem
polynomial.map_expand
{R : Type u}
[comm_semiring R]
{S : Type v}
[comm_semiring S]
{p : ℕ}
{f : R →+* S}
{q : polynomial R} :
polynomial.map f (⇑(polynomial.expand R p) q) = ⇑(polynomial.expand S p) (polynomial.map f q)
@[simp]
theorem
polynomial.expand_eval
{R : Type u}
[comm_semiring R]
(p : ℕ)
(P : polynomial R)
(r : R) :
polynomial.eval r (⇑(polynomial.expand R p) P) = polynomial.eval (r ^ p) P
@[simp]
theorem
polynomial.expand_aeval
{R : Type u}
[comm_semiring R]
{A : Type u_1}
[semiring A]
[algebra R A]
(p : ℕ)
(P : polynomial R)
(r : A) :
⇑(polynomial.aeval r) (⇑(polynomial.expand R p) P) = ⇑(polynomial.aeval (r ^ p)) P
The opposite of expand: sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.
Equations
- polynomial.contract p f = (finset.range (f.nat_degree + 1)).sum (λ (n : ℕ), ⇑(polynomial.monomial n) (f.coeff (n * p)))
theorem
polynomial.coeff_contract
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : p ≠ 0)
(f : polynomial R)
(n : ℕ) :
(polynomial.contract p f).coeff n = f.coeff (n * p)
theorem
polynomial.contract_expand
{R : Type u}
[comm_semiring R]
(p : ℕ)
{f : polynomial R}
(hp : p ≠ 0) :
polynomial.contract p (⇑(polynomial.expand R p) f) = f
theorem
polynomial.expand_contract
{R : Type u}
[comm_semiring R]
(p : ℕ)
[char_p R p]
[no_zero_divisors R]
{f : polynomial R}
(hf : ⇑polynomial.derivative f = 0)
(hp : p ≠ 0) :
⇑(polynomial.expand R p) (polynomial.contract p f) = f
theorem
polynomial.expand_char
{R : Type u}
[comm_semiring R]
(p : ℕ)
[char_p R p]
[hp : fact (nat.prime p)]
(f : polynomial R) :
polynomial.map (frobenius R p) (⇑(polynomial.expand R p) f) = f ^ p
theorem
polynomial.map_expand_pow_char
{R : Type u}
[comm_semiring R]
(p : ℕ)
[char_p R p]
[hp : fact (nat.prime p)]
(f : polynomial R)
(n : ℕ) :
polynomial.map (frobenius R p ^ n) (⇑(polynomial.expand R (p ^ n)) f) = f ^ p ^ n
theorem
polynomial.of_irreducible_expand
{R : Type u}
[comm_ring R]
[is_domain R]
{p : ℕ}
(hp : p ≠ 0)
{f : polynomial R}
(hf : irreducible (⇑(polynomial.expand R p) f)) :
theorem
polynomial.of_irreducible_expand_pow
{R : Type u}
[comm_ring R]
[is_domain R]
{p : ℕ}
(hp : p ≠ 0)
{f : polynomial R}
{n : ℕ} :
irreducible (⇑(polynomial.expand R (p ^ n)) f) → irreducible f