Formal power series (in one variable) - Order

The PowerSeries.order of a formal power series φ is the multiplicity of the variable X in φ.

If the coefficients form an integral domain, then PowerSeries.order is an additive valuation (PowerSeries.order_mul, PowerSeries.min_order_le_order_add).

We prove that if the commutative ring R of coefficients is an integral domain, then the ring R⟦X⟧ of formal power series in one variable over R is an integral domain.

Given a non-zero power series f, divided_by_X_pow_order f is the power series obtained by dividing out the largest power of X that divides f, that is its order. This is useful when proving that R⟦X⟧ is a normalization monoid, which is done in PowerSeries.Inverse.

theorem PowerSeries.exists_coeff_ne_zero_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : (∃ (n : ℕ), (coeff n) φ ≠ 0) ↔ φ ≠ 0

noncomputable def PowerSeries.order {R : Type u_1} [Semiring R] (φ : PowerSeries R) : ℕ∞

The order of a formal power series φ is the greatest n : ℕ∞ such that X^n divides φ. The order is ⊤ if and only if φ = 0.

Equations

• φ.order = if h : φ = 0 then ⊤ else ↑(Nat.find ⋯)

@[simp]

theorem PowerSeries.order_zero {R : Type u_1} [Semiring R] : order 0 = ⊤

The order of the 0 power series is infinite.

theorem PowerSeries.order_finite_iff_ne_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : φ.order < ⊤ ↔ φ ≠ 0

@[simp]

theorem PowerSeries.order_eq_top {R : Type u_1} [Semiring R] {φ : PowerSeries R} : φ.order = ⊤ ↔ φ = 0

The 0 power series is the unique power series with infinite order.

theorem PowerSeries.coe_toNat_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (hf : φ ≠ 0) : ↑φ.order.toNat = φ.order

theorem PowerSeries.coeff_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (h : φ ≠ 0) : (coeff φ.order.toNat) φ ≠ 0

If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.

theorem PowerSeries.order_le {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : (coeff n) φ ≠ 0) : φ.order ≤ ↑n

If the nth coefficient of a formal power series is nonzero, then the order of the power series is less than or equal to n.

theorem PowerSeries.coeff_of_lt_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : ↑n < φ.order) : (coeff n) φ = 0

The nth coefficient of a formal power series is 0 if n is strictly smaller than the order of the power series.

theorem PowerSeries.coeff_of_lt_order_toNat {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (h : n < φ.order.toNat) : (coeff n) φ = 0

theorem PowerSeries.nat_le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ) (h : ∀ i < n, (coeff i) φ = 0) : ↑n ≤ φ.order

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

theorem PowerSeries.le_order {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ∞) (h : ∀ (i : ℕ), ↑i < n → (coeff i) φ = 0) : n ≤ φ.order

The order of a formal power series is at least n if the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq_nat {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ} : φ.order = ↑n ↔ (coeff n) φ ≠ 0 ∧ ∀ i < n, (coeff i) φ = 0

The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq {R : Type u_1} [Semiring R] {φ : PowerSeries R} {n : ℕ∞} : φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (coeff i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (coeff i) φ = 0

The order of a formal power series is exactly n if the nth coefficient is nonzero, and the ith coefficient is 0 for all i < n.

theorem PowerSeries.order_eq_order {R : Type u_1} [Semiring R] {φ : PowerSeries R} : φ.order = MvPowerSeries.order φ

theorem PowerSeries.min_order_le_order_add {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : min φ.order ψ.order ≤ (φ + ψ).order

The order of the sum of two formal power series is at least the minimum of their orders.

theorem PowerSeries.order_add_of_order_ne {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) (h : φ.order ≠ ψ.order) : (φ + ψ).order = min φ.order ψ.order

The order of the sum of two formal power series is the minimum of their orders if their orders differ.

@[deprecated PowerSeries.order_add_of_order_ne (since := "2025-09-17")]

theorem PowerSeries.order_add_of_order_eq {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) (h : φ.order ≠ ψ.order) : (φ + ψ).order = min φ.order ψ.order

Alias of PowerSeries.order_add_of_order_ne.

---

The order of the sum of two formal power series is the minimum of their orders if their orders differ.

theorem PowerSeries.le_order_map {R : Type u_1} [Semiring R] {φ : PowerSeries R} {S : Type u_2} [Semiring S] (f : R →+* S) : φ.order ≤ ((map f) φ).order

theorem PowerSeries.le_order_smul {R : Type u_1} [Semiring R] {φ : PowerSeries R} {a : R} : φ.order ≤ (a • φ).order

theorem PowerSeries.le_order_mul {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : φ.order + ψ.order ≤ (φ * ψ).order

The order of the product of two formal power series is at least the sum of their orders.

theorem PowerSeries.le_order_pow {R : Type u_1} [Semiring R] (φ : PowerSeries R) (n : ℕ) : n • φ.order ≤ (φ ^ n).order

theorem PowerSeries.le_order_prod {R : Type u_2} [CommSemiring R] {ι : Type u_3} (φ : ι → PowerSeries R) (s : Finset ι) : ∑ i ∈ s, (φ i).order ≤ (∏ i ∈ s, φ i).order

theorem PowerSeries.order_mul_ge {R : Type u_1} [Semiring R] (φ ψ : PowerSeries R) : φ.order + ψ.order ≤ (φ * ψ).order

Alias of PowerSeries.le_order_mul.

---

The order of the product of two formal power series is at least the sum of their orders.

theorem PowerSeries.one_le_order_iff_constCoeff_eq_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : 1 ≤ φ.order ↔ constantCoeff φ = 0

theorem PowerSeries.order_ne_zero_iff_constCoeff_eq_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} : φ.order ≠ 0 ↔ constantCoeff φ = 0

theorem PowerSeries.le_order_pow_of_constantCoeff_eq_zero {R : Type u_1} [Semiring R] {φ : PowerSeries R} (n : ℕ) (hf : constantCoeff φ = 0) : ↑n ≤ (φ ^ n).order

theorem PowerSeries.order_monomial {R : Type u_1} [Semiring R] (n : ℕ) (a : R) [Decidable (a = 0)] : ((monomial n) a).order = if a = 0 then ⊤ else ↑n

The order of the monomial a*X^n is infinite if a = 0 and n otherwise.

theorem PowerSeries.order_monomial_of_ne_zero {R : Type u_1} [Semiring R] (n : ℕ) (a : R) (h : a ≠ 0) : ((monomial n) a).order = ↑n

The order of the monomial a*X^n is n if a ≠ 0.

theorem PowerSeries.coeff_mul_of_lt_order {R : Type u_1} [Semiring R] {φ ψ : PowerSeries R} {n : ℕ} (h : ↑n < ψ.order) : (coeff n) (φ * ψ) = 0

If n is strictly smaller than the order of ψ, then the nth coefficient of its product with any other power series is 0.

theorem PowerSeries.coeff_mul_one_sub_of_lt_order {R : Type u_2} [Ring R] {φ ψ : PowerSeries R} (n : ℕ) (h : ↑n < ψ.order) : (coeff n) (φ * (1 - ψ)) = (coeff n) φ

theorem PowerSeries.coeff_mul_prod_one_sub_of_lt_order {R : Type u_2} {ι : Type u_3} [CommRing R] (k : ℕ) (s : Finset ι) (φ : PowerSeries R) (f : ι → PowerSeries R) : (∀ i ∈ s, ↑k < (f i).order) → (coeff k) (φ * ∏ i ∈ s, (1 - f i)) = (coeff k) φ

@[simp]

theorem PowerSeries.order_neg {R : Type u_2} [Ring R] (φ : PowerSeries R) : (-φ).order = φ.order

noncomputable def PowerSeries.divXPowOrder {R : Type u_1} [Semiring R] (f : PowerSeries R) : PowerSeries R

Given a non-zero power series f, divXPowOrder f is the power series obtained by dividing out the largest power of X that divides f, that is its order

Equations

• f.divXPowOrder = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff (n + f.order.toNat)) f

@[simp]

theorem PowerSeries.coeff_divXPowOrder {R : Type u_1} [Semiring R] {f : PowerSeries R} {n : ℕ} : (coeff n) f.divXPowOrder = (coeff (n + f.order.toNat)) f

@[simp]

theorem PowerSeries.divXPowOrder_zero {R : Type u_1} [Semiring R] : divXPowOrder 0 = 0

theorem PowerSeries.constantCoeff_divXPowOrder {R : Type u_1} [Semiring R] {f : PowerSeries R} : constantCoeff f.divXPowOrder = (coeff f.order.toNat) f

theorem PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff {R : Type u_1} [Semiring R] {f : PowerSeries R} : constantCoeff f.divXPowOrder = 0 ↔ f = 0

theorem PowerSeries.X_pow_order_mul_divXPowOrder {R : Type u_1} [Semiring R] {f : PowerSeries R} : X ^ f.order.toNat * f.divXPowOrder = f

theorem PowerSeries.X_pow_order_dvd {R : Type u_1} [Semiring R] {φ : PowerSeries R} : X ^ φ.order.toNat ∣ φ

theorem PowerSeries.order_eq_emultiplicity_X {R : Type u_2} [Semiring R] (φ : PowerSeries R) : φ.order = emultiplicity X φ

@[simp]

theorem PowerSeries.order_one {R : Type u_1} [Semiring R] [Nontrivial R] : order 1 = 0

The order of the formal power series 1 is 0.

theorem PowerSeries.order_zero_of_unit {R : Type u_1} [Semiring R] [Nontrivial R] {f : PowerSeries R} : IsUnit f → f.order = 0

The order of an invertible power series is 0.

@[simp]

theorem PowerSeries.order_X {R : Type u_1} [Semiring R] [Nontrivial R] : X.order = 1

The order of the formal power series X is 1.

@[simp]

theorem PowerSeries.order_X_pow {R : Type u_1} [Semiring R] [Nontrivial R] (n : ℕ) : (X ^ n).order = ↑n

The order of the formal power series X^n is n.

@[simp]

theorem PowerSeries.divXPowOrder_X {R : Type u_1} [Semiring R] [Nontrivial R] : X.divXPowOrder = 1

Dividing X by the maximal power of X dividing it leaves 1.

theorem PowerSeries.divXPowOrder_one {R : Type u_1} [Semiring R] [Nontrivial R] : divXPowOrder 1 = 1

theorem PowerSeries.order_mul {R : Type u_1} [Semiring R] [NoZeroDivisors R] (φ ψ : PowerSeries R) : (φ * ψ).order = φ.order + ψ.order

The order of the product of two formal power series over an integral domain is the sum of their orders.

theorem PowerSeries.divXPowOrder_mul {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f g : PowerSeries R} : (f * g).divXPowOrder = f.divXPowOrder * g.divXPowOrder

The operation of dividing a power series by the largest possible power of X preserves multiplication.

@[deprecated PowerSeries.divXPowOrder_mul "use `divXPowOrder_mul.symm` instead" (since := "2025-11-06")]

theorem PowerSeries.divXPowOrder_mul_divXPowOrder {R : Type u_1} [Semiring R] [NoZeroDivisors R] {f g : PowerSeries R} : f.divXPowOrder * g.divXPowOrder = (f * g).divXPowOrder

noncomputable def PowerSeries.orderHom {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] : PowerSeries R →* Multiplicative ℕ∞

PowerSeries.order as a MonoidHom.

Equations

• PowerSeries.orderHom = { toFun := fun (g : PowerSeries R) => Multiplicative.ofAdd g.order, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem PowerSeries.coe_orderHom {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] : ⇑orderHom = order

theorem PowerSeries.order_pow {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (φ : PowerSeries R) (n : ℕ) : (φ ^ n).order = n • φ.order

theorem PowerSeries.order_prod {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_3} (φ : ι → PowerSeries R) (s : Finset ι) : (∏ i ∈ s, φ i).order = ∑ i ∈ s, (φ i).order

noncomputable def PowerSeries.divXPowOrderHom {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] : PowerSeries R →* PowerSeries R

PowerSeries.divXPowOrder as a MonoidHom.

Equations

• PowerSeries.divXPowOrderHom = { toFun := fun (g : PowerSeries R) => g.divXPowOrder, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem PowerSeries.coe_divXPowOrderHom {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] : ⇑divXPowOrderHom = divXPowOrder

theorem PowerSeries.divXPowOrder_pow {R : Type u_1} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (φ : PowerSeries R) (n : ℕ) : (φ ^ n).divXPowOrder = φ.divXPowOrder ^ n

theorem PowerSeries.divXPowOrder_prod {R : Type u_2} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_3} (φ : ι → PowerSeries R) (s : Finset ι) : (∏ i ∈ s, φ i).divXPowOrder = ∏ i ∈ s, (φ i).divXPowOrder

@[simp]

theorem PowerSeries.order_toSubring {R : Type u_1} [Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ (n : ℕ), (coeff n) p ∈ T) : (p.toSubring T hp).order = p.order