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ⁿ.

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 = let __src := Polynomial.eval₂RingHom Polynomial.C (Polynomial.X ^ p); { toRingHom := __src, commutes' := ⋯ }

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 = Polynomial.comp f (Polynomial.X ^ p)

theorem Polynomial.expand_eq_sum {R : Type u} [CommSemiring R] (p : ℕ) {f : Polynomial R} : (Polynomial.expand R p) f = Polynomial.sum f fun (e : ℕ) (a : R) => Polynomial.C a * (Polynomial.X ^ p) ^ e

@[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.coeff ((Polynomial.expand R p) f) n = if p ∣ n then Polynomial.coeff f (n / p) else 0

@[simp]

theorem Polynomial.coeff_expand_mul {R : Type u} [CommSemiring R] {p : ℕ} (hp : 0 < p) (f : Polynomial R) (n : ℕ) : Polynomial.coeff ((Polynomial.expand R p) f) (n * p) = Polynomial.coeff f n

@[simp]

theorem Polynomial.coeff_expand_mul' {R : Type u} [CommSemiring R] {p : ℕ} (hp : 0 < p) (f : Polynomial R) (n : ℕ) : Polynomial.coeff ((Polynomial.expand R p) f) (p * n) = Polynomial.coeff f n

theorem Polynomial.expand_injective {R : Type u} [CommSemiring R] {n : ℕ} (hn : 0 < n) : Function.Injective ⇑(Polynomial.expand R 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.natDegree ((Polynomial.expand R p) f) = Polynomial.natDegree f * p

theorem Polynomial.leadingCoeff_expand {R : Type u} [CommSemiring R] {p : ℕ} {f : Polynomial R} (hp : 0 < p) : Polynomial.leadingCoeff ((Polynomial.expand R p) f) = Polynomial.leadingCoeff f

theorem Polynomial.monic_expand_iff {R : Type u} [CommSemiring R] {p : ℕ} {f : Polynomial R} (hp : 0 < p) : Polynomial.Monic ((Polynomial.expand R p) f) ↔ Polynomial.Monic f

theorem Polynomial.Monic.expand {R : Type u} [CommSemiring R] {p : ℕ} {f : Polynomial R} (hp : 0 < p) : Polynomial.Monic f → Polynomial.Monic ((Polynomial.expand R p) f)

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

noncomputable def Polynomial.contract {R : Type u} [CommSemiring R] (p : ℕ) (f : Polynomial R) : Polynomial R

The opposite of expand: sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.

Equations

• Polynomial.contract p f = Finset.sum (Finset.range (Polynomial.natDegree f + 1)) fun (n : ℕ) => (Polynomial.monomial n) (Polynomial.coeff f (n * p))

theorem Polynomial.coeff_contract {R : Type u} [CommSemiring R] {p : ℕ} (hp : p ≠ 0) (f : Polynomial R) (n : ℕ) : Polynomial.coeff (Polynomial.contract p f) n = Polynomial.coeff f (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)) : Irreducible 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