Expand power series

Given a power series φ, one may replace every occurrence of X i by X i ^ n, for some nonzero natural number n. This operation is called PowerSeries.expand and it is an algebra homomorphism.

Main declaration

• PowerSeries.expand: expand a power series by a nonzero factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

noncomputable def PowerSeries.expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) : PowerSeries R →ₐ[R] PowerSeries R

Expand the power series by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

See also PowerSeries.expand.

Equations

• PowerSeries.expand p hp = MvPowerSeries.expand p hp

theorem PowerSeries.expand_apply {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (f : PowerSeries R) : (expand p hp) f = subst (X ^ p) f

theorem PowerSeries.expand_C {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (r : R) : (expand p hp) (C r) = C r

theorem PowerSeries.expand_mul_eq_comp {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0) : expand (p * q) ⋯ = (expand p hp).comp (expand q hq)

theorem PowerSeries.expand_mul {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (q : ℕ) (hq : q ≠ 0) (φ : PowerSeries R) : (expand (p * q) ⋯) φ = (expand p hp) ((expand q hq) φ)

theorem PowerSeries.expand_smul {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (a : R) (φ : PowerSeries R) : (expand p hp) (a • φ) = a • (expand p hp) φ

@[simp]

theorem PowerSeries.expand_X {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) : (expand p hp) X = X ^ p

@[simp]

theorem PowerSeries.expand_monomial {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (d : ℕ) (r : R) : (expand p hp) ((monomial d) r) = (monomial (p * d)) r

@[simp]

theorem PowerSeries.expand_one {R : Type u_2} [CommRing R] : expand 1 ⋯ = AlgHom.id R (PowerSeries R)

theorem PowerSeries.expand_one_apply {R : Type u_2} [CommRing R] (f : PowerSeries R) : (expand 1 ⋯) f = f

@[simp]

theorem PowerSeries.map_expand {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] (p : ℕ) (hp : p ≠ 0) (f : R →+* S) (φ : PowerSeries R) : (map f) ((expand p hp) φ) = (expand p hp) ((map f) φ)

theorem PowerSeries.expand_subst {τ : Type u_1} {S : Type u_3} [CommRing S] (p : ℕ) (hp : p ≠ 0) {f : MvPowerSeries τ S} (hf : HasSubst f) (φ : PowerSeries S) : (MvPowerSeries.expand p hp) (subst f φ) = subst ((MvPowerSeries.expand p hp) f) φ

@[simp]

theorem PowerSeries.coeff_expand_mul {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) (m : ℕ) : (coeff (p * m)) ((expand p hp) φ) = (coeff m) φ

@[simp]

theorem PowerSeries.constantCoeff_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) : constantCoeff ((expand p hp) φ) = constantCoeff φ

theorem PowerSeries.coeff_expand_of_not_dvd {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) {m : ℕ} (h : ¬p ∣ m) : (coeff m) ((expand p hp) φ) = 0

theorem PowerSeries.support_expand_subset {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) : Function.support ((expand p hp) φ) ⊆ (fun (x : Unit →₀ ℕ) => p • x) '' Function.support φ

theorem PowerSeries.support_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) : Function.support ((expand p hp) φ) = (fun (x : Unit →₀ ℕ) => p • x) '' Function.support φ

theorem PowerSeries.coeff_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) {n : ℕ} : (coeff n) ((expand p hp) φ) = if p ∣ n then (coeff (n / p)) φ else 0

@[simp]

theorem PowerSeries.order_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R) : ((expand p hp) φ).order = p • φ.order

theorem PowerSeries.map_frobenius_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) [ExpChar R p] {f : PowerSeries R} : (map (frobenius R p)) ((expand p hp) f) = f ^ p

theorem PowerSeries.map_iterateFrobenius_expand {R : Type u_2} [CommRing R] (p : ℕ) (hp : p ≠ 0) [ExpChar R p] (f : PowerSeries R) (n : ℕ) : (map (iterateFrobenius R p n)) ((expand (p ^ n) ⋯) f) = f ^ p ^ n

theorem FiniteField.PowerSeries.expand_card {K : Type u_4} [Field K] [Fintype K] (f : PowerSeries K) : (PowerSeries.expand (Fintype.card K) ⋯) f = f ^ Fintype.card K