Dividing Formal Power Series

This file formalizes the content from DividingFPS.tex, covering:

• Inverses in commutative rings (uniqueness, notation)
• Characterization of invertible FPSs
• Newton's binomial formula for FPSs
• Upper negation formula for binomial coefficients
• Division by x for FPSs with vanishing constant term
• Various lemmas about coefficients and multiples

Main Results

• fps_invertible_iff_constantCoeff: An FPS is invertible iff its constant term is invertible
• fps_invertible_iff_constantCoeff_ne_zero: Over a field, an FPS is invertible iff its constant term is nonzero
• binomUpperNegation: The upper negation formula C(-n,k) = (-1)^k * C(k+n-1,k)
• fps_onePlusX_inv: Formula for (1+x)^{-1} as a power series
• fps_onePlusX_pow_neg: Formula for (1+x)^{-n} for natural n
• fps_newtonBinomial: Newton's binomial formula (1+x)^n = Σ C(n,k) x^k
• PowerSeries.divByX: Division by x for FPSs with zero constant term
• Various lemmas about coefficients and multiples of FPSs

References

• Grinberg, Darij. "Algebraic Combinatorics" (lecture notes)

Tags

formal power series, inverses, binomial coefficients, Newton's binomial formula

Section: Conventions

We identify each element a ∈ K with the constant FPS (a, 0, 0, 0, ...). In Mathlib, this is handled via the ring homomorphism algebraMap K (PowerSeries K).

@[reducible, inline]

abbrev AlgebraicCombinatorics.constFPS {K : Type u_1} [CommRing K] (a : K) : PowerSeries K

The constant FPS corresponding to an element of the base ring. This is algebraMap K (PowerSeries K) in Mathlib.

Equations

• AlgebraicCombinatorics.constFPS a = (algebraMap K (PowerSeries K)) a

Section: Inverses in commutative rings

The uniqueness of inverses and notation for fractions are standard in Mathlib. We recall the key facts here for reference.

theorem AlgebraicCombinatorics.inverse_unique {L : Type u_2} [CommRing L] {a b c : L} (hb : a * b = 1) (hc : a * c = 1) : b = c

Theorem (thm.commring.inverse-uni): In a commutative ring, inverses are unique. If a * b = 1 and a * c = 1, then b = c. This follows from Mathlib's left_inv_eq_right_inv.

theorem AlgebraicCombinatorics.inverse_unique_of_isUnit {L : Type u_2} [CommRing L] {a : L} (ha : IsUnit a) {b : L} (hb : a * b = 1) : b = ↑ha.unit⁻¹

Variant of inverse_unique: if a is a unit, any element b with a * b = 1 equals the canonical inverse ha.unit⁻¹.

Section: Properties of inverses and fractions (prop.commring.fracs.1)

Proposition (prop.commring.fracs.1): Let L be a commutative ring. Then:

• (a) Any invertible element a ∈ L satisfies a⁻¹ = 1/a.
• (b) For any invertible elements a, b ∈ L, the element ab is invertible as well, and satisfies (ab)⁻¹ = b⁻¹a⁻¹ = a⁻¹b⁻¹.
• (c) If a ∈ L is invertible, and if n ∈ ℤ is arbitrary, then a^{-n} = (a⁻¹)^n = (a^n)⁻¹.
• (d) Laws of exponents hold for negative exponents as well.
• (e) Laws of fractions hold: b/a + d/c = (bc + ad)/(ac) and (b/a) · (d/c) = (bd)/(ac).
• (f) Division undoes multiplication: c/a = b iff c = ab.

In Mathlib, these are mostly standard lemmas for Units and IsUnit.

theorem AlgebraicCombinatorics.fracs1_inv_eq_one_mul_inv {L : Type u_2} [CommRing L] (u : Lˣ) : u⁻¹ = 1 * u⁻¹

Proposition (prop.commring.fracs.1a): For an invertible element a, the inverse a⁻¹ equals 1/a (i.e., 1 * a⁻¹). This is essentially definitional in Mathlib.

theorem AlgebraicCombinatorics.fracs1_isUnit_mul {L : Type u_2} [CommRing L] {a b : L} (ha : IsUnit a) (hb : IsUnit b) : IsUnit (a * b)

Proposition (prop.commring.fracs.1b): If a and b are invertible, then a * b is invertible.

theorem AlgebraicCombinatorics.fracs1_mul_inv_rev {L : Type u_2} [CommRing L] (u v : Lˣ) : (u * v)⁻¹ = v⁻¹ * u⁻¹

Proposition (prop.commring.fracs.1b): (a * b)⁻¹ = b⁻¹ * a⁻¹ for units.

theorem AlgebraicCombinatorics.fracs1_mul_inv_comm {L : Type u_2} [CommRing L] (u v : Lˣ) : (u * v)⁻¹ = u⁻¹ * v⁻¹

Proposition (prop.commring.fracs.1b): In a commutative ring, (a * b)⁻¹ = a⁻¹ * b⁻¹ for units.

theorem AlgebraicCombinatorics.fracs1_zpow_neg_eq_inv_zpow {L : Type u_2} [CommRing L] (u : Lˣ) (n : ℤ) : u ^ (-n) = u⁻¹ ^ n

Proposition (prop.commring.fracs.1c): For a unit u and integer n, u^{-n} = (u⁻¹)^n.

theorem AlgebraicCombinatorics.fracs1_zpow_neg_eq_zpow_inv {L : Type u_2} [CommRing L] (u : Lˣ) (n : ℤ) : u ^ (-n) = (u ^ n)⁻¹

Proposition (prop.commring.fracs.1c): For a unit u and integer n, u^{-n} = (u^n)⁻¹.

theorem AlgebraicCombinatorics.fracs1_zpow_add {L : Type u_2} [CommRing L] (u : Lˣ) (n m : ℤ) : u ^ (n + m) = u ^ n * u ^ m

Proposition (prop.commring.fracs.1d): a^{n+m} = a^n * a^m for all integers n, m.

theorem AlgebraicCombinatorics.fracs1_mul_zpow {L : Type u_2} [CommRing L] (u v : Lˣ) (n : ℤ) : (u * v) ^ n = u ^ n * v ^ n

Proposition (prop.commring.fracs.1d): (a * b)^n = a^n * b^n for all integers n.

theorem AlgebraicCombinatorics.fracs1_zpow_mul {L : Type u_2} [CommRing L] (u : Lˣ) (n m : ℤ) : (u ^ n) ^ m = u ^ (n * m)

Proposition (prop.commring.fracs.1d): (a^n)^m = a^{nm} for all integers n, m.

def AlgebraicCombinatorics.divByUnit {L : Type u_2} [CommRing L] (b : L) (a : Lˣ) : L

Division notation for units: b / a means b * a⁻¹. This formalizes the notation b/a for a invertible in the text.

Equations

• AlgebraicCombinatorics.divByUnit b a = b * ↑a⁻¹

def AlgebraicCombinatorics.«term_/ᵤ_» : Lean.TrailingParserDescr

Local notation for division by a unit.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.fracs1_div_add_div {L : Type u_2} [CommRing L] (a c : Lˣ) (b d : L) : divByUnit b a + divByUnit d c = divByUnit (b * ↑c + ↑a * d) (a * c)

Proposition (prop.commring.fracs.1e): b/a + d/c = (bc + ad)/(ac).

theorem AlgebraicCombinatorics.fracs1_div_mul_div {L : Type u_2} [CommRing L] (a c : Lˣ) (b d : L) : divByUnit b a * divByUnit d c = divByUnit (b * d) (a * c)

Proposition (prop.commring.fracs.1e): (b/a) * (d/c) = (bd)/(ac).

theorem AlgebraicCombinatorics.fracs1_div_eq_iff {L : Type u_2} [CommRing L] (a : Lˣ) (b c : L) : divByUnit c a = b ↔ c = ↑a * b

Proposition (prop.commring.fracs.1f): c/a = b iff c = a * b.

Section: Inverses in K[[x]]

Proposition (prop.fps.invertible): An FPS a is invertible in K[[x]] if and only if its constant term [x^0] a is invertible in K.

This is PowerSeries.isUnit_iff_constantCoeff in Mathlib.

theorem AlgebraicCombinatorics.fps_invertible_iff_constantCoeff {K : Type u_1} [CommRing K] (a : PowerSeries K) : IsUnit a ↔ IsUnit (PowerSeries.constantCoeff a)

An FPS is invertible iff its constant term is invertible. Label: prop.fps.invertible

theorem AlgebraicCombinatorics.fps_invertible_iff_constantCoeff_ne_zero {F : Type u_2} [Field F] (a : PowerSeries F) : IsUnit a ↔ PowerSeries.constantCoeff a ≠ 0

Corollary (cor.fps.invertible.field): Over a field, an FPS is invertible iff its constant term is nonzero. Label: cor.fps.invertible.field

Section: Coefficient formulas for inverses

Explicit formulas for the coefficients of the inverse of an FPS.

theorem AlgebraicCombinatorics.fps_inv_coeff_zero {F : Type u_2} [Field F] (f : PowerSeries F) : (PowerSeries.coeff 0) f⁻¹ = ((PowerSeries.coeff 0) f)⁻¹

The constant term of the inverse of an FPS equals the inverse of its constant term. This is a direct corollary of Mathlib's PowerSeries.constantCoeff_inv. Label: fps_inv_coeff_zero

theorem AlgebraicCombinatorics.fps_inv_coeff_succ {F : Type u_2} [Field F] (f : PowerSeries F) (n : ℕ) : (PowerSeries.coeff (n + 1)) f⁻¹ = -((PowerSeries.coeff 0) f)⁻¹ * ∑ k ∈ Finset.range (n + 1), (PowerSeries.coeff (k + 1)) f * (PowerSeries.coeff (n - k)) f⁻¹

Recurrence for coefficients of the inverse of an FPS. For n > 0: [x^n]f⁻¹ = -(f₀)⁻¹ · ∑_{k=1}^n f_k · [x^{n-k}]f⁻¹

This is a reformulation of Mathlib's PowerSeries.coeff_inv that expresses the recurrence in terms of a sum over Finset.range (n + 1) with shifted indices, which matches the standard textbook formula.

The recurrence shows that each coefficient of f⁻¹ can be computed from:

• The constant term f₀ (which must be nonzero for f to be invertible)
• The coefficients f₁, f₂, ..., f_n of f
• The previously computed coefficients [x^0]f⁻¹, [x^1]f⁻¹, ..., [x^{n-1}]f⁻¹

Label: fps_inv_coeff_succ

theorem AlgebraicCombinatorics.fps_isUnit_inv_eq_inv {F : Type u_2} [Field F] (f : PowerSeries F) (hf : IsUnit f) : ↑hf.unit⁻¹ = f⁻¹

Helper lemma: For an invertible FPS f, the unit inverse hf.unit⁻¹ equals f⁻¹. This connects the IsUnit formulation with the direct inverse.

theorem AlgebraicCombinatorics.fps_inv_coeff_zero_isUnit {F : Type u_2} [Field F] (f : PowerSeries F) (hf : IsUnit f) : (PowerSeries.coeff 0) ↑hf.unit⁻¹ = ((PowerSeries.coeff 0) f)⁻¹

The constant term of the inverse of an invertible FPS equals the inverse of its constant term. This is the IsUnit version of fps_inv_coeff_zero. Label: fps_inv_coeff_zero_isUnit

theorem AlgebraicCombinatorics.fps_inv_coeff_succ_isUnit {F : Type u_2} [Field F] (f : PowerSeries F) (hf : IsUnit f) (n : ℕ) : (PowerSeries.coeff (n + 1)) ↑hf.unit⁻¹ = -((PowerSeries.coeff 0) f)⁻¹ * ∑ k ∈ Finset.range (n + 1), (PowerSeries.coeff (k + 1)) f * (PowerSeries.coeff (n - k)) ↑hf.unit⁻¹

Recurrence for coefficients of the inverse of an invertible FPS. This is the IsUnit version of fps_inv_coeff_succ. Label: fps_inv_coeff_succ_isUnit

Section: Newton's binomial formula

We prove Newton's binomial formula: (1+x)^n = Σ_{k ∈ ℕ} C(n,k) x^k for all n ∈ ℤ.

theorem AlgebraicCombinatorics.fps_onePlusX_isUnit {K : Type u_1} [CommRing K] : IsUnit (1 + PowerSeries.X)

Proposition (prop.fps.invertible.1+x): The FPS 1+x is invertible, with inverse 1 - x + x^2 - x^3 + .... Label: prop.fps.invertible.1+x

theorem AlgebraicCombinatorics.fps_onePlusX_inv {F : Type u_2} [Field F] : (1 + PowerSeries.X)⁻¹ = PowerSeries.mk fun (n : ℕ) => (-1) ^ n

The inverse of 1+x is Σ_{n ∈ ℕ} (-1)^n x^n. Note: This requires K to be a field to have Inv instance on PowerSeries K. Label: prop.fps.invertible.1+x

theorem AlgebraicCombinatorics.binomUpperNegation {R : Type u_2} [CommRing R] [BinomialRing R] [NatPowAssoc R] (r : R) (k : ℕ) : Ring.choose (-r) k = (-1) ^ k * Ring.choose (r + ↑k - 1) k

Theorem (thm.binom.upneg-n): Upper negation formula for binomial coefficients. For r in a BinomialRing R and k ∈ ℕ, we have C(-r, k) = (-1)^k * C(r+k-1, k).

Note: In Mathlib, generalized binomial coefficients are defined via Ring.choose for BinomialRings. This generalizes the classical formula for n ∈ ℂ. Label: thm.binom.upneg-n

theorem AlgebraicCombinatorics.binomUpperNegation_int (n : ℤ) (k : ℕ) : Ring.choose (-n) k = (-1) ^ k * Ring.choose (↑k + n - 1) k

Specialization of binomUpperNegation to integers. For n ∈ ℤ and k ∈ ℕ, we have C(-n, k) = (-1)^k * C(k+n-1, k). Label: thm.binom.upneg-n

theorem AlgebraicCombinatorics.fps_onePlusX_pow_neg {F : Type u_2} [Field F] [BinomialRing F] (n : ℕ) : (1 + PowerSeries.X)⁻¹ ^ n = PowerSeries.mk fun (k : ℕ) => (-1) ^ k * ↑(Ring.choose (↑n + ↑k - 1) k)

Proposition (prop.fps.anti-newton-binom): For each n ∈ ℕ, we have (1+x)^{-n} = Σ_{k ∈ ℕ} (-1)^k * C(n+k-1, k) * x^k.

Note: We express this using the inverse since PowerSeries over a general ring doesn't have integer power operations. Label: prop.fps.anti-newton-binom

theorem AlgebraicCombinatorics.fps_onePlusX_pow_neg' {F : Type u_2} [Field F] [BinomialRing F] (n : ℕ) : (1 + PowerSeries.X)⁻¹ ^ n = PowerSeries.mk fun (k : ℕ) => Ring.choose (-↑↑n) k

Corollary (cor.fps.anti-newton-binom-2): For each n ∈ ℕ, we have (1+x)^{-n} = Σ_{k ∈ ℕ} C(-n, k) * x^k. Label: cor.fps.anti-newton-binom-2

theorem AlgebraicCombinatorics.fps_newtonBinomial_nat {R : Type u_2} [CommRing R] (n : ℕ) : (1 + PowerSeries.X) ^ n = PowerSeries.mk fun (k : ℕ) => if k ≤ n then ↑(n.choose k) else 0

Theorem (thm.fps.newton-binom): Newton's binomial formula. For each n ∈ ℕ, we have (1+x)^n = Σ_{k ∈ ℕ} C(n,k) x^k.

Note: For non-negative integers, this follows from the standard binomial theorem. Label: thm.fps.newton-binom

theorem AlgebraicCombinatorics.fps_newtonBinomial_neg {F : Type u_2} [Field F] [BinomialRing F] (n : ℕ) : (1 + PowerSeries.X)⁻¹ ^ n = PowerSeries.mk fun (k : ℕ) => Ring.choose (-↑↑n) k

Newton's binomial formula for negative integer exponents over a field. The inverse of (1+x)^n equals Σ C(-n,k) x^k. Label: thm.fps.newton-binom

Section: Dividing by x

Definition (def.fps.div-by-x): For an FPS a = (a_0, a_1, a_2, ...) with a_0 = 0, we define a/x to be the FPS (a_1, a_2, a_3, ...).

def AlgebraicCombinatorics.PowerSeries.divByX {K : Type u_1} [CommRing K] (a : PowerSeries K) : PowerSeries.constantCoeff a = 0 → PowerSeries K

Division of an FPS by x, defined when the constant term is zero. Given a = (a_0, a_1, a_2, ...) with a_0 = 0, returns (a_1, a_2, a_3, ...). Label: def.fps.div-by-x

Equations

• AlgebraicCombinatorics.PowerSeries.divByX a x✝ = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff (n + 1)) a

@[simp]

theorem AlgebraicCombinatorics.PowerSeries.coeff_divByX {K : Type u_1} [CommRing K] (a : PowerSeries K) (ha : PowerSeries.constantCoeff a = 0) (n : ℕ) : (PowerSeries.coeff n) (divByX a ha) = (PowerSeries.coeff (n + 1)) a

The coefficient of x^n in a/x is the coefficient of x^{n+1} in a.

theorem AlgebraicCombinatorics.fps_eq_X_mul_iff {K : Type u_1} [CommRing K] (a b : PowerSeries K) : a = PowerSeries.X * b ↔ PowerSeries.constantCoeff a = 0 ∧ ∃ (h : PowerSeries.constantCoeff a = 0), b = PowerSeries.divByX a h

Proposition (prop.fps.div-by-x-inverts): a = x * b iff a has zero constant term and b = a/x. Label: prop.fps.div-by-x-inverts

@[simp]

theorem AlgebraicCombinatorics.fps_X_mul_constantCoeff_zero {K : Type u_1} [CommRing K] (b : PowerSeries K) : PowerSeries.constantCoeff (PowerSeries.X * b) = 0

X * b has zero constant term. Label: prop.fps.div-by-x-inverts (helper)

theorem AlgebraicCombinatorics.fps_eq_X_mul_divByX {K : Type u_1} [CommRing K] (a : PowerSeries K) (ha : PowerSeries.constantCoeff a = 0) : a = PowerSeries.X * PowerSeries.divByX a ha

If a.constantCoeff = 0, then a = X * (a/x). Label: prop.fps.div-by-x-inverts (helper)

theorem AlgebraicCombinatorics.fps_divByX_X_mul {K : Type u_1} [CommRing K] (b : PowerSeries K) : PowerSeries.divByX (PowerSeries.X * b) ⋯ = b

(X * b) / X = b. Label: prop.fps.div-by-x-inverts (helper)

theorem AlgebraicCombinatorics.fps_exists_X_mul_of_constantCoeff_zero {K : Type u_1} [CommRing K] (a : PowerSeries K) (ha : PowerSeries.constantCoeff a = 0) : ∃ (h : PowerSeries K), a = PowerSeries.X * h

Lemma (lem.fps.g=xh): If an FPS a has zero constant term, then there exists an FPS h such that a = x * h. Label: lem.fps.g=xh

Section: A few lemmas

Various lemmas about coefficients and multiples of FPSs.

theorem AlgebraicCombinatorics.fps_coeff_X_pow_mul_eq_zero {K : Type u_1} [CommRing K] (k : ℕ) (a : PowerSeries K) (m : ℕ) (hm : m < k) : (PowerSeries.coeff m) (PowerSeries.X ^ k * a) = 0

Lemma (lem.fps.first-n-coeffs-of-xna): The first k coefficients of x^k * a are zero. Label: lem.fps.first-n-coeffs-of-xna

theorem AlgebraicCombinatorics.fps_first_k_coeffs_zero_iff_X_pow_dvd {K : Type u_1} [CommRing K] (k : ℕ) (f : PowerSeries K) : (∀ m < k, (PowerSeries.coeff m) f = 0) ↔ PowerSeries.X ^ k ∣ f

Lemma (lem.fps.muls-of-xn): The first k coefficients of f are zero iff f is a multiple of x^k. Label: lem.fps.muls-of-xn

def AlgebraicCombinatorics.PowerSeries.isMultipleOf {K : Type u_1} [CommRing K] (f g : PowerSeries K) : Prop

A multiple of g is an FPS of the form g * a.

Equations

• AlgebraicCombinatorics.PowerSeries.isMultipleOf f g = (g ∣ f)

theorem AlgebraicCombinatorics.fps_coeff_mul_eq_of_coeff_eq {K : Type u_1} [CommRing K] (a f g : PowerSeries K) (n : ℕ) (h : ∀ m ≤ n, (PowerSeries.coeff m) f = (PowerSeries.coeff m) g) (m : ℕ) : m ≤ n → (PowerSeries.coeff m) (a * f) = (PowerSeries.coeff m) (a * g)

Lemma (lem.fps.prod.irlv.fg): If the first n+1 coefficients of f and g agree, then the first n+1 coefficients of a*f and a*g agree. Label: lem.fps.prod.irlv.fg

theorem AlgebraicCombinatorics.fps_coeff_zero_of_multiple {K : Type u_1} [CommRing K] (u v : PowerSeries K) (n : ℕ) (hdvd : u ∣ v) (hu : ∀ m ≤ n, (PowerSeries.coeff m) u = 0) (m : ℕ) : m ≤ n → (PowerSeries.coeff m) v = 0

Lemma (lem.fps.prod.irlv.mul): If v is a multiple of u, and the first n+1 coefficients of u are zero, then the first n+1 coefficients of v are zero. Label: lem.fps.prod.irlv.mul

theorem AlgebraicCombinatorics.fps_coeff_mul_eq_of_both_coeff_eq {K : Type u_1} [CommRing K] (a b c d : PowerSeries K) (n : ℕ) (hab : ∀ m ≤ n, (PowerSeries.coeff m) a = (PowerSeries.coeff m) b) (hcd : ∀ m ≤ n, (PowerSeries.coeff m) c = (PowerSeries.coeff m) d) (m : ℕ) : m ≤ n → (PowerSeries.coeff m) (a * c) = (PowerSeries.coeff m) (b * d)

Lemma (lem.fps.prod.irlv.cong-mul): If the first n+1 coefficients of a and b agree, and the first n+1 coefficients of c and d agree, then the first n+1 coefficients of a*c and b*d agree. Label: lem.fps.prod.irlv.cong-mul