Expand a polynomial by a factor of p, so ∑ aₙ xⁿ
becomes ∑ aₙ xⁿᵖ
. #
Main definitions #
Polynomial.expand R p f
: expand the polynomialf
with coefficients in a commutative semiringR
by 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)
[CommSemiring 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 = { toRingHom := Polynomial.eval₂RingHom Polynomial.C (Polynomial.X ^ p), commutes' := ⋯ }
Instances For
theorem
Polynomial.coe_expand
(R : Type u)
[CommSemiring R]
(p : ℕ)
:
⇑(Polynomial.expand R p) = Polynomial.eval₂ Polynomial.C (Polynomial.X ^ p)
theorem
Polynomial.expand_eq_comp_X_pow
{R : Type u}
[CommSemiring R]
(p : ℕ)
{f : Polynomial R}
:
(Polynomial.expand R p) f = f.comp (Polynomial.X ^ p)
@[simp]
theorem
Polynomial.expand_C
{R : Type u}
[CommSemiring R]
(p : ℕ)
(r : R)
:
(Polynomial.expand R p) (Polynomial.C r) = Polynomial.C r
@[simp]
theorem
Polynomial.expand_X
{R : Type u}
[CommSemiring R]
(p : ℕ)
:
(Polynomial.expand R p) Polynomial.X = Polynomial.X ^ p
@[simp]
theorem
Polynomial.expand_monomial
{R : Type u}
[CommSemiring 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}
[CommSemiring 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}
[CommSemiring 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}
[CommSemiring R]
(f : Polynomial R)
:
(Polynomial.expand R 0) f = Polynomial.C (Polynomial.eval 1 f)
@[simp]
theorem
Polynomial.expand_one
{R : Type u}
[CommSemiring R]
(f : Polynomial R)
:
(Polynomial.expand R 1) f = f
theorem
Polynomial.expand_pow
{R : Type u}
[CommSemiring 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}
[CommSemiring 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}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
(f : Polynomial R)
(n : ℕ)
:
((Polynomial.expand R p) f).coeff n = if p ∣ n then f.coeff (n / p) else 0
@[simp]
theorem
Polynomial.coeff_expand_mul
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
(f : Polynomial R)
(n : ℕ)
:
((Polynomial.expand R p) f).coeff (n * p) = f.coeff n
@[simp]
theorem
Polynomial.coeff_expand_mul'
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
(f : Polynomial R)
(n : ℕ)
:
((Polynomial.expand R p) f).coeff (p * n) = f.coeff n
Expansion is injective.
theorem
Polynomial.expand_inj
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
{f : Polynomial R}
{g : Polynomial R}
:
(Polynomial.expand R p) f = (Polynomial.expand R p) g ↔ f = g
theorem
Polynomial.expand_eq_zero
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
{f : Polynomial R}
:
(Polynomial.expand R p) f = 0 ↔ f = 0
theorem
Polynomial.expand_ne_zero
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
{f : Polynomial R}
:
(Polynomial.expand R p) f ≠ 0 ↔ f ≠ 0
theorem
Polynomial.expand_eq_C
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : 0 < p)
{f : Polynomial R}
{r : R}
:
(Polynomial.expand R p) f = Polynomial.C r ↔ f = Polynomial.C r
theorem
Polynomial.natDegree_expand
{R : Type u}
[CommSemiring R]
(p : ℕ)
(f : Polynomial R)
:
((Polynomial.expand R p) f).natDegree = f.natDegree * p
theorem
Polynomial.leadingCoeff_expand
{R : Type u}
[CommSemiring R]
{p : ℕ}
{f : Polynomial R}
(hp : 0 < p)
:
((Polynomial.expand R p) f).leadingCoeff = f.leadingCoeff
theorem
Polynomial.monic_expand_iff
{R : Type u}
[CommSemiring R]
{p : ℕ}
{f : Polynomial R}
(hp : 0 < p)
:
((Polynomial.expand R p) f).Monic ↔ f.Monic
theorem
Polynomial.Monic.expand
{R : Type u}
[CommSemiring R]
{p : ℕ}
{f : Polynomial R}
(hp : 0 < p)
:
f.Monic → ((Polynomial.expand R p) f).Monic
Alias of the reverse direction of Polynomial.monic_expand_iff
.
theorem
Polynomial.map_expand
{R : Type u}
[CommSemiring R]
{S : Type v}
[CommSemiring 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}
[CommSemiring 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}
[CommSemiring 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 = ∑ n ∈ Finset.range (f.natDegree + 1), (Polynomial.monomial n) (f.coeff (n * p))
Instances For
theorem
Polynomial.coeff_contract
{R : Type u}
[CommSemiring R]
{p : ℕ}
(hp : p ≠ 0)
(f : Polynomial R)
(n : ℕ)
:
(Polynomial.contract p f).coeff n = f.coeff (n * p)
theorem
Polynomial.map_contract
{R : Type u}
[CommSemiring R]
{S : Type v}
[CommSemiring S]
{p : ℕ}
(hp : p ≠ 0)
{f : R →+* S}
{q : Polynomial R}
:
Polynomial.map f (Polynomial.contract p q) = Polynomial.contract p (Polynomial.map f q)
theorem
Polynomial.contract_expand
{R : Type u}
[CommSemiring R]
(p : ℕ)
{f : Polynomial R}
(hp : p ≠ 0)
:
Polynomial.contract p ((Polynomial.expand R p) f) = f
theorem
Polynomial.contract_one
{R : Type u}
[CommSemiring R]
{f : Polynomial R}
:
Polynomial.contract 1 f = f
theorem
Polynomial.expand_contract
{R : Type u}
[CommSemiring R]
(p : ℕ)
[CharP R p]
[NoZeroDivisors R]
{f : Polynomial R}
(hf : Polynomial.derivative f = 0)
(hp : p ≠ 0)
:
(Polynomial.expand R p) (Polynomial.contract p f) = f
theorem
Polynomial.expand_contract'
{R : Type u}
[CommSemiring R]
(p : ℕ)
[ExpChar R p]
[NoZeroDivisors R]
{f : Polynomial R}
(hf : Polynomial.derivative f = 0)
:
(Polynomial.expand R p) (Polynomial.contract p f) = f
theorem
Polynomial.expand_char
{R : Type u}
[CommSemiring R]
(p : ℕ)
[ExpChar R 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}
[CommSemiring R]
(p : ℕ)
[ExpChar R p]
(f : Polynomial R)
(n : ℕ)
:
Polynomial.map (frobenius R p ^ n) ((Polynomial.expand R (p ^ n)) f) = f ^ p ^ n
theorem
Polynomial.rootMultiplicity_expand_pow
{R : Type u}
[CommRing R]
{p : ℕ}
{n : ℕ}
[ExpChar R p]
{f : Polynomial R}
{r : R}
:
Polynomial.rootMultiplicity r ((Polynomial.expand R (p ^ n)) f) = p ^ n * Polynomial.rootMultiplicity (r ^ p ^ n) f
theorem
Polynomial.rootMultiplicity_expand
{R : Type u}
[CommRing R]
{p : ℕ}
[ExpChar R p]
{f : Polynomial R}
{r : R}
:
Polynomial.rootMultiplicity r ((Polynomial.expand R p) f) = p * Polynomial.rootMultiplicity (r ^ p) f
theorem
Polynomial.isLocalRingHom_expand
(R : Type u)
[CommRing R]
[IsDomain R]
{p : ℕ}
(hp : 0 < p)
:
IsLocalRingHom ↑(Polynomial.expand R p)
theorem
Polynomial.of_irreducible_expand
{R : Type u}
[CommRing R]
[IsDomain R]
{p : ℕ}
(hp : p ≠ 0)
{f : Polynomial R}
(hf : Irreducible ((Polynomial.expand R p) f))
:
theorem
Polynomial.of_irreducible_expand_pow
{R : Type u}
[CommRing R]
[IsDomain R]
{p : ℕ}
(hp : p ≠ 0)
{f : Polynomial R}
{n : ℕ}
:
Irreducible ((Polynomial.expand R (p ^ n)) f) → Irreducible f