1.4 Dividing FPSs

1.4.1 Inverses in commutative rings

Definition 1.107

✓

Let \(L\) be a commutative ring. Let \(a\in L\). Then:

(a) An inverse (or multiplicative inverse) of \(a\) means an element \(b\in L\) such that \(ab=ba=1\).

(b) We say that \(a\) is invertible in \(L\) (or a unit of \(L\)) if \(a\) has an inverse.

docs source

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 1.108

✓

Let \(L\) be a commutative ring. Let \(a\in L\). Then, there is at most one inverse of \(a\).

docs source

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

b = c

Proof ▶

Let \(b\) and \(c\) be two inverses of \(a\). Since \(b\) is an inverse of \(a\), we have \(ab=ba=1\). Since \(c\) is an inverse of \(a\), we have \(ac=ca=1\). Now, \(b\left(ac\right) = b\cdot 1 = b\) and \(\left(ba\right)c = 1\cdot c = c\). However, \(b\left(ac\right) = \left(ba\right)c\) by associativity. Hence, \(b = b\left(ac\right) = \left(ba\right)c = c\).

Definition 1.109

✓

Let \(L\) be a commutative ring. Let \(a\in L\). Assume that \(a\) is invertible. Then:

(a) The inverse of \(a\) is called \(a^{-1}\).

(b) For any \(b\in L\), the product \(b\cdot a^{-1}\) is called \(\frac{b}{a}\) (or \(b/a\)).

(c) For any negative integer \(n\), we define \(a^{n}\) to be \(\left( a^{-1}\right)^{-n}\). Thus, the \(n\)-th power \(a^{n}\) is defined for each \(n\in \mathbb {Z}\).

docs source

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

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

Proposition 1.110

Let \(L\) be a commutative ring. Then:

(a) Any invertible element \(a\in L\) satisfies \(a^{-1}=1/a\).

(b) For any invertible elements \(a,b\in L\), the element \(ab\) is invertible as well, and satisfies \(\left(ab\right)^{-1}=b^{-1}a^{-1}=a^{-1}b^{-1}\).

(c) If \(a\in L\) is invertible, and if \(n\in \mathbb {Z}\) is arbitrary, then \(a^{-n}=\left(a^{-1}\right)^{n}=\left(a^{n}\right)^{-1}\).

(d) Laws of exponents hold for negative exponents as well: If \(a\) and \(b\) are invertible elements of \(L\), then

\begin{align*} a^{n+m} & =a^{n}a^{m}\ \ \ \ \ \ \ \ \ \ \text{for all }n,m\in \mathbb {Z};\\ \left( ab\right) ^{n} & =a^{n}b^{n}\ \ \ \ \ \ \ \ \ \ \text{for all }n\in \mathbb {Z};\\ \left( a^{n}\right) ^{m} & =a^{nm}\ \ \ \ \ \ \ \ \ \ \text{for all }n,m\in \mathbb {Z}. \end{align*}

(e) Laws of fractions hold: If \(a\) and \(c\) are two invertible elements of \(L\), and if \(b\) and \(d\) are any two elements of \(L\), then

\[ \frac{b}{a}+\frac{d}{c}=\frac{bc+ad}{ac}\ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \frac{b}{a}\cdot \frac{d}{c}=\frac{bd}{ac}. \]

(f) Division undoes multiplication: If \(a,b,c\) are three elements of \(L\) with \(a\) being invertible, then the equality \(\frac{c}{a}=b\) is equivalent to \(c=ab\).

docs source

theorem AlgebraicCombinatorics.fracs1_inv_eq_one_mul_inv {L : Type u_2} [CommRing L] (u : Lˣ) :

u⁻¹ = 1 * u⁻¹

docs source

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

IsUnit (a * b)

docs source

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

(u * v)⁻¹ = v⁻¹ * u⁻¹

docs source

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

(u * v)⁻¹ = u⁻¹ * v⁻¹

docs source

theorem AlgebraicCombinatorics.fracs1_zpow_neg_eq_inv_zpow {L : Type u_2} [CommRing L] (u : Lˣ) (n : ℤ) :

u ^ (-n) = u⁻¹ ^ n

docs source

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

u ^ (n + m) = u ^ n * u ^ m

docs source

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

(u * v) ^ n = u ^ n * v ^ n

docs source

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

(u ^ n) ^ m = u ^ (n * m)

docs source

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)

docs source

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)

docs source

theorem AlgebraicCombinatorics.fracs1_div_eq_iff {L : Type u_2} [CommRing L] (a : Lˣ) (b c : L) :

divByUnit c a = b ↔ c = ↑a * b

Proof ▶

Exercise (see, e.g., [ 19s , solution to Exercise 4.1.1 ] for a proof of parts (c) and (d) in the special case where \(L=\mathbb {C}\); essentially the same argument works in the general case).

1.4.2 Inverses in \(K[[x]]\)

Proposition 1.111

✓

Let \(a\in K[[x]]\). Then, the FPS \(a\) is invertible in \(K[[x]]\) if and only if its constant term \([x^{0}]a\) is invertible in \(K\).

docs source

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

IsUnit a ↔ IsUnit (PowerSeries.constantCoeff a)

Proof ▶

\(\Longrightarrow \): If \(ab=1\), then \([x^0]a\cdot [x^0]b = [x^0](ab)=1\) (by Lemma 1.87).

\(\Longleftarrow \): If \([x^0]a = a_0\) is invertible, define a sequence \((b_0, b_1, b_2, \ldots )\) recursively by \(b_0 = a_0^{-1}\) (Lemma 1.113) and \(b_n = -a_0^{-1}\sum _{k=1}^n a_k b_{n-k}\) for \(n \geq 1\) (Lemma 1.114). Then \(ab = 1\).

Corollary 1.112

✓

Assume that \(K\) is a field. Let \(a\in K[[x]]\). Then, the FPS \(a\) is invertible in \(K[[x]]\) if and only if \([x^{0}]a\neq 0\).

docs source

theorem AlgebraicCombinatorics.fps_invertible_iff_constantCoeff_ne_zero {F : Type u_2} [Field F] (a : PowerSeries F) :

IsUnit a ↔ PowerSeries.constantCoeff a ≠ 0

Proof ▶

An element of \(K\) is invertible in \(K\) if and only if it is nonzero (since \(K\) is a field). Hence, Corollary 1.112 follows from Proposition 1.111.

1.4.3 Coefficient formulas for inverses

Lemma 1.113

Assume that \(K\) is a field. Let \(f\in K[[x]]\). Then the constant term of \(f^{-1}\) equals the inverse of the constant term of \(f\):

\[ \left[x^{0}\right]f^{-1} = \left(\left[x^{0}\right]f\right)^{-1}. \]

docs source

theorem AlgebraicCombinatorics.fps_inv_coeff_zero {F : Type u_2} [Field F] (f : PowerSeries F) :

(PowerSeries.coeff 0) f⁻¹ = ((PowerSeries.coeff 0) f)⁻¹

Proof ▶

Direct consequence of the definition of the inverse of an FPS.

Lemma 1.114

Assume that \(K\) is a field. Let \(f\in K[[x]]\). For each \(n\in \mathbb {N}\),

\[ \left[x^{n+1}\right]f^{-1} = -\left(\left[x^{0}\right]f\right)^{-1}\sum _{k=0}^{n}\left[x^{k+1}\right]f\cdot \left[x^{n-k}\right]f^{-1}. \]

This recurrence allows computing the coefficients of \(f^{-1}\) one by one.

docs source

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⁻¹

Proof ▶

Follows from the recurrence relation for the coefficients of \(f^{-1}\) obtained by expanding the equation \(f\cdot f^{-1}=1\) and solving for \([x^{n+1}]f^{-1}\).

Lemma 1.115

✓

Assume that \(K\) is a field. Let \(f\in K[[x]]\) be an invertible FPS. Then the inverse of \(f\) obtained from the invertibility proof equals \(f^{-1}\) (the inverse as defined in the power series ring).

docs source

theorem AlgebraicCombinatorics.fps_isUnit_inv_eq_inv {F : Type u_2} [Field F] (f : PowerSeries F) (hf : IsUnit f) :

↑hf.unit⁻¹ = f⁻¹

Proof ▶

Both satisfy \(f\cdot g = 1\), and inverses are unique (Theorem 1.108).

Lemma 1.116

✓

Assume that \(K\) is a field. Let \(f\in K[[x]]\) be an invertible FPS. Then

\[ \left[x^{0}\right]f^{-1} = \left(\left[x^{0}\right]f\right)^{-1}. \]

docs source

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)⁻¹

Proof ▶

By Lemma 1.115, the inverse obtained from the invertibility proof equals \(f^{-1}\), so the result follows from Lemma 1.113.

Lemma 1.117

Assume that \(K\) is a field. Let \(f\in K[[x]]\) be an invertible FPS. For each \(n\in \mathbb {N}\),

\[ \left[x^{n+1}\right]f^{-1} = -\left(\left[x^{0}\right]f\right)^{-1}\sum _{k=0}^{n}\left[x^{k+1}\right]f\cdot \left[x^{n-k}\right]f^{-1}. \]

docs source

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⁻¹

Proof ▶

By Lemma 1.115, the inverse obtained from the invertibility proof equals \(f^{-1}\), so the result follows from Lemma 1.114.

1.4.4 Newton’s binomial formula

Proposition 1.118

✓

The FPS \(1+x\in K[[x]]\) is invertible, and its inverse is

\[ \left(1+x\right)^{-1}=\sum _{n\in \mathbb {N}}\left(-1\right)^{n}x^{n}. \]

docs source

theorem AlgebraicCombinatorics.fps_onePlusX_isUnit {K : Type u_1} [CommRing K] :

IsUnit (1 + PowerSeries.X)

docs source

theorem AlgebraicCombinatorics.fps_onePlusX_inv {F : Type u_2} [Field F] :

(1 + PowerSeries.X)⁻¹ = PowerSeries.mk fun (n : ℕ) => (-1) ^ n

Proof ▶

Direct computation: \((1+x)\cdot \sum _{n\geq 0}(-1)^n x^n = 1\) by telescoping (all powers of \(x\) other than \(1\) cancel out).

Theorem 1.119

✓

For each \(n\in \mathbb {Z}\), we have

\[ \left(1+x\right)^{n}=\sum _{k\in \mathbb {N}}\binom {n}{k}x^{k}. \]

docs source

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

docs source

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

Proof ▶

For \(n\geq 0\), this is the standard binomial theorem (the sum \(\sum _{k\in \mathbb {N}}\binom {n}{k}x^{k}\) reduces to \(\sum _{k=0}^{n}\binom {n}{k}x^{k}\) since \(\binom {n}{k}=0\) for \(k {\gt} n\) by Proposition 1.8).

For \(n{\lt}0\), we have \(-n\in \mathbb {N}\), so Corollary 1.122 (applied to \(-n\) instead of \(n\)) yields \(\left(1+x\right)^{-(-n)} = \sum _{k\in \mathbb {N}}\binom {-(-n)}{k}x^k\), which rewrites as \(\left(1+x\right)^n = \sum _{k\in \mathbb {N}}\binom {n}{k}x^k\).

Theorem 1.120

✓

Let \(n\in \mathbb {C}\) and \(k\in \mathbb {Z}\). Then,

\[ \binom {-n}{k}=\left(-1\right)^{k}\binom {k+n-1}{k}. \]

docs source

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

docs source

theorem AlgebraicCombinatorics.binomUpperNegation_int (n : ℤ) (k : ℕ) :

Ring.choose (-n) k = (-1) ^ k * Ring.choose (↑k + n - 1) k

Proof ▶

If \(k{\lt}0\), then both \(\binom {-n}{k}\) and \(\binom {k+n-1}{k}\) are \(0\). For \(k\geq 0\), expand using the definition and observe the numerators differ by a factor of \((-1)^k\).

Proposition 1.121

For each \(n\in \mathbb {N}\), we have

\[ \left(1+x\right)^{-n}=\sum _{k\in \mathbb {N}}\left(-1\right)^{k}\binom {n+k-1}{k}x^{k}. \]

docs source

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)

Proof ▶

By induction on \(n\).

Induction base: \(\left(1+x\right)^{-0} = 1\), and \(\sum _{k\in \mathbb {N}} (-1)^k \binom {0+k-1}{k} x^k = 1\) since \(\binom {k-1}{k} = 0\) for all \(k {\gt} 0\) (by Proposition 1.8).

Induction step: Assume the formula holds for \(n = j\). We must prove it for \(n = j+1\). We have \(\left(1+x\right)^{-(j+1)} = \left(1+x\right)^{-j} \cdot \left(1+x\right)^{-1}\). Using the induction hypothesis and multiplying by \(1+x\), it suffices to show

\[ \left(1+x\right)^{-j} = \left(\sum _{k\in \mathbb {N}} (-1)^k \binom {j+k}{k} x^k\right) \cdot \left(1+x\right). \]

Expanding the right hand side, using Pascal’s identity \(\binom {j+k}{k} = \binom {j+k-1}{k-1} + \binom {j+k-1}{k}\) (Proposition 1.5), and collecting terms (the \(\binom {j+k-1}{k-1}\) terms telescope), we obtain \(\sum _{k\in \mathbb {N}} (-1)^k \binom {j+k-1}{k} x^k = \left(1+x\right)^{-j}\) by the induction hypothesis.

Corollary 1.122

✓

For each \(n\in \mathbb {N}\), we have

\[ \left(1+x\right)^{-n}=\sum _{k\in \mathbb {N}}\binom {-n}{k}x^{k}. \]

docs source

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

Proof ▶

Proposition 1.121 yields \(\left(1+x\right)^{-n} = \sum _{k\in \mathbb {N}} (-1)^k \binom {n+k-1}{k} x^k\). By Theorem 1.120, we have \((-1)^k \binom {n+k-1}{k} = (-1)^k \binom {k+n-1}{k} = \binom {-n}{k}\).

1.4.5 Dividing by \(x\)

Definition 1.123

✓

Let \(a=\left(a_{0},a_{1},a_{2},\ldots \right)\) be an FPS whose constant term \(a_{0}\) is \(0\). Then, \(\frac{a}{x}\) is defined to be the FPS \(\left(a_{1},a_{2},a_{3},\ldots \right)\).

docs source

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

PowerSeries.constantCoeff a = 0 → PowerSeries K

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

Lemma 1.124

✓

Let \(a\in K[[x]]\) with \([x^0]a=0\). Then for each \(n\in \mathbb {N}\),

\[ \left[x^{n}\right]\frac{a}{x} = \left[x^{n+1}\right]a. \]

docs source

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

Proof ▶

By definition, \(\frac{a}{x}=(a_1,a_2,a_3,\ldots )\), so its \(n\)-th coefficient is \(a_{n+1}=[x^{n+1}]a\).

Proposition 1.125

✓

Let \(a,b\in K[[x]]\) be two FPSs. Then, \(a=xb\) if and only if \(\left[x^{0}\right]a=0\) and \(b=\frac{a}{x}\).

docs source

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

Proof ▶

Follows directly from the definitions.

Helpers for division by \(x\)

Lemma 1.126

✓

Let \(a\in K[[x]]\) with \([x^0]a=0\). Then \(a = x\cdot \frac{a}{x}\).

docs source

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

Proof ▶

Follows from Proposition 1.125: setting \(b=\frac{a}{x}\), the right-to-left direction gives \(a=xb\).

Lemma 1.127

✓

For any FPS \(b\in K[[x]]\), we have \(\frac{xb}{x}=b\).

docs source

theorem AlgebraicCombinatorics.fps_divByX_X_mul {K : Type u_1} [CommRing K] (b : PowerSeries K) :

PowerSeries.divByX (PowerSeries.X * b) ⋯ = b

Proof ▶

For each \(n\in \mathbb {N}\), \([x^n]\frac{xb}{x}=[x^{n+1}](xb)=[x^n]b\) (by Lemma 1.124 and the coefficient formula for \(xb\)).

1.4.6 A few lemmas

Lemma 1.128

✓

Let \(a\in K[[x]]\) be an FPS with \(\left[x^{0}\right]a=0\). Then, there exists an \(h\in K[[x]]\) such that \(a=xh\).

docs source

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

Proof ▶

The FPS \(\frac{a}{x}\) is well-defined (since \(a_0 = 0\)). Set \(h = \frac{a}{x}\); then \(a = x \cdot \frac{a}{x} = xh\) (by Lemma 1.126).

Lemma 1.129

✓

Let \(k\in \mathbb {N}\). Let \(a\in K[[x]]\) be any FPS. Then, the first \(k\) coefficients of the FPS \(x^{k}a\) are \(0\).

docs source

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

Proof ▶

For \(m{\lt}k\), we have \([x^m](x^k a) = \sum _{i=0}^{m} [x^i](x^k)\cdot [x^{m-i}]a = 0\) since \([x^i](x^k) = 0\) for all \(i\leq m {\lt} k\).

Lemma 1.130

✓

Let \(k\in \mathbb {N}\). Let \(f\in K[[x]]\) be any FPS. Then, the first \(k\) coefficients of \(f\) are \(0\) if and only if \(f\) is a multiple of \(x^{k}\).

docs source

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

Proof ▶

\(\Longleftarrow \): By Lemma 1.129.

\(\Longrightarrow \): If \(f_n = 0\) for each \(n \in \{ 0, 1, \ldots , k-1\} \), then \(f = \sum _{n \geq k} f_n x^n = x^k \sum _{n \geq k} f_n x^{n-k}\).

Lemma 1.131

✓

Let \(a,f,g\in K[[x]]\) be three FPSs. Let \(n\in \mathbb {N}\). Assume that \([x^{m}]f=[x^{m}]g\) for each \(m\in \{ 0,1,\ldots ,n\} \). Then, \([x^{m}](af)=[x^{m}](ag)\) for each \(m\in \{ 0,1,\ldots ,n\} \).

docs source

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)

Proof ▶

Let \(m \in \{ 0,1,\ldots ,n\} \). Each \(j \in \{ 0,1,\ldots ,m\} \) satisfies \(j \leq m \leq n\) and thus \([x^j]f = [x^j]g\). Hence, \([x^m](af) = \sum _{j=0}^m [x^{m-j}]a \cdot [x^j]f = \sum _{j=0}^m [x^{m-j}]a \cdot [x^j]g = [x^m](ag)\).

Lemma 1.132

✓

Let \(u,v\in K[[x]]\) be two FPSs such that \(v\) is a multiple of \(u\). Let \(n\in \mathbb {N}\). Assume \([x^{m}]u=0\) for each \(m\in \{ 0,1,\ldots ,n\} \). Then \([x^{m}]v=0\) for each \(m\in \{ 0,1,\ldots ,n\} \).

docs source

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

Proof ▶

Write \(v=ua\). We have \([x^m]u = 0 = [x^m]0\) for each \(m \in \{ 0,1,\ldots ,n\} \). Lemma 1.131 (applied to \(f=u\) and \(g=0\)) yields \([x^m](au) = [x^m](a \cdot 0) = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \). Since \(v = ua = au\), we get \([x^m]v = 0\).

Lemma 1.133

✓

Let \(a,b,c,d\in K[[x]]\) be four FPSs. Let \(n\in \mathbb {N}\). Assume \([x^{m}]a=[x^{m}]b\) and \([x^{m}]c=[x^{m}]d\) for each \(m\in \{ 0,1,\ldots ,n\} \). Then \([x^{m}](ac)=[x^{m}](bd)\) for each \(m\in \{ 0,1,\ldots ,n\} \).

docs source

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)

Proof ▶

The FPS \(ac - bc = (a-b)c\) is a multiple of \(a-b\), and \([x^m](a-b) = 0\) for each \(m \in \{ 0,1,\ldots ,n\} \). By Lemma 1.132, \([x^m](ac - bc) = 0\), so \([x^m](ac) = [x^m](bc)\).

Similarly, \(bc - bd = b(c-d) = (c-d)b\) is a multiple of \(c-d\), and \([x^m](c-d) = 0\). By Lemma 1.132, \([x^m](bc - bd) = 0\), so \([x^m](bc) = [x^m](bd)\).

Combining: \([x^m](ac) = [x^m](bc) = [x^m](bd)\).