Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg

1.11 \(x^{n}\)-equivalence

Definition 1.322
✓
#

Let \(n\in \mathbb {N}\). Let \(f,g\in K\left[\left[x\right]\right]\) be two FPSs. We write \(f\overset {x^{n}}{\equiv }g\) if and only if

\[ \text{each }m\in \left\{ 0,1,\ldots ,n\right\} \text{ satisfies } \left[x^{m}\right]f=\left[x^{m}\right]g. \]

Thus, we have defined a binary relation \(\overset {x^{n}}{\equiv }\) on the set \(K\left[\left[x\right]\right]\). We say that an FPS \(f\) is \(x^{n}\)-equivalent to an FPS \(g\) if and only if \(f\overset {x^{n}}{\equiv }g\).

def PowerSeries.XnEquiv {R : Type u_1} [CommSemiring R] (n : ℕ) (f g : PowerSeries R) :
Lemma 1.323
✓

Let \(m,n\in \mathbb {N}\) with \(m\leq n\). If \(f\overset {x^{n}}{\equiv }g\), then \(f\overset {x^{m}}{\equiv }g\).

theorem PowerSeries.XnEquiv.of_le {R : Type u_1} [CommSemiring R] {m n : ℕ} (hmn : m ≤ n) {f g : PowerSeries R} (h : f ≡[x^n] g) :
f ≡[x^m] g
Proof ▶

If each \(k\in \{ 0,1,\ldots ,n\} \) satisfies \([x^k]f=[x^k]g\), then in particular each \(k\in \{ 0,1,\ldots ,m\} \subseteq \{ 0,1,\ldots ,n\} \) satisfies \([x^k]f=[x^k]g\).

Lemma 1.324
✓

Two FPSs \(f,g\in K[[x]]\) satisfy \(f\overset {x^{0}}{\equiv }g\) if and only if \([x^0]f=[x^0]g\).

Proof ▶

This is immediate from the definition, since \(\{ 0,1,\ldots ,0\} =\{ 0\} \).

1.11.1 Helpers for the equivalence relation

Lemma 1.325
✓

Let \(n\in \mathbb {N}\). For any FPS \(f\in K[[x]]\), we have \(f\overset {x^{n}}{\equiv }f\).

theorem PowerSeries.XnEquiv.refl {R : Type u_1} [CommSemiring R] (n : ℕ) (f : PowerSeries R) :
f ≡[x^n] f
Proof ▶

Immediate from the definition: \([x^m]f=[x^m]f\) for all \(m\).

Lemma 1.326
✓

Let \(n\in \mathbb {N}\). If \(f,g\in K[[x]]\) satisfy \(f\overset {x^{n}}{\equiv }g\), then \(g\overset {x^{n}}{\equiv }f\).

theorem PowerSeries.XnEquiv.symm {R : Type u_1} [CommSemiring R] {n : ℕ} {f g : PowerSeries R} (h : f ≡[x^n] g) :
g ≡[x^n] f
Proof ▶

If \([x^m]f=[x^m]g\) for all \(m\leq n\), then \([x^m]g=[x^m]f\) by symmetry of equality.

Lemma 1.327
✓

Let \(n\in \mathbb {N}\). If \(f,g,h\in K[[x]]\) satisfy \(f\overset {x^{n}}{\equiv }g\) and \(g\overset {x^{n}}{\equiv }h\), then \(f\overset {x^{n}}{\equiv }h\).

theorem PowerSeries.XnEquiv.trans {R : Type u_1} [CommSemiring R] {n : ℕ} {f g h : PowerSeries R} (hfg : f ≡[x^n] g) (hgh : g ≡[x^n] h) :
f ≡[x^n] h
Proof ▶

If \([x^m]f=[x^m]g\) and \([x^m]g=[x^m]h\) for all \(m\leq n\), then \([x^m]f=[x^m]h\) by transitivity of equality.

Theorem 1.328

Let \(n\in \mathbb {N}\).

(a) The relation \(\overset {x^{n}}{\equiv }\) on \(K\left[\left[ x\right]\right]\) is an equivalence relation. In other words:

  • This relation is reflexive (i.e., we have \(f\overset {x^{n}}{\equiv }f\) for each \(f\in K\left[\left[x\right]\right]\)).

  • This relation is transitive (i.e., if three FPSs \(f,g,h\in K\left[ \left[x\right]\right]\) satisfy \(f\overset {x^{n}}{\equiv }g\) and \(g\overset {x^{n}}{\equiv }h\), then \(f\overset {x^{n}}{\equiv }h\)).

  • This relation is symmetric (i.e., if two FPSs \(f,g\in K\left[\left[ x\right]\right]\) satisfy \(f\overset {x^{n}}{\equiv }g\), then \(g\overset {x^{n}}{\equiv }f\)).

(b) If \(a,b,c,d\in K\left[\left[x\right]\right]\) are four FPSs satisfying \(a\overset {x^{n}}{\equiv }b\) and \(c\overset {x^{n}}{\equiv }d\), then we also have

\begin{align} & a+c\overset {x^{n}}{\equiv }b+d;\label{eq.thm.fps.xneq.props.b.+}\\ & a-c\overset {x^{n}}{\equiv }b-d;\label{eq.thm.fps.xneq.props.b.-}\\ & ac\overset {x^{n}}{\equiv }bd. \label{eq.thm.fps.xneq.props.b.*} \end{align}

(c) If \(a,b\in K\left[\left[x\right]\right]\) are two FPSs satisfying \(a\overset {x^{n}}{\equiv }b\), then \(\lambda a\overset {x^{n}}{\equiv }\lambda b\) for each \(\lambda \in K\).

(d) If \(a,b\in K\left[\left[x\right]\right]\) are two invertible FPSs satisfying \(a\overset {x^{n}}{\equiv }b\), then \(a^{-1} \overset {x^{n}}{\equiv }b^{-1}\).

(e) If \(a,b,c,d\in K\left[\left[x\right]\right]\) are four FPSs satisfying \(a\overset {x^{n}}{\equiv }b\) and \(c\overset {x^{n}}{\equiv }d\), and if the FPSs \(c\) and \(d\) are invertible, then we also have

\begin{equation} \frac{a}{c}\overset {x^{n}}{\equiv }\frac{b}{d}. \label{eq.thm.fps.xneq.props.e./} \end{equation}
58

(f) Let \(S\) be a finite set. Let \(\left(a_{s}\right)_{s\in S}\in K\left[\left[x\right]\right]^{S}\) and \(\left(b_{s}\right)_{s\in S}\in K\left[\left[x\right]\right]^{S}\) be two families of FPSs such that

\begin{equation} \text{each }s\in S\text{ satisfies }a_{s}\overset {x^{n}}{\equiv }b_{s}. \label{eq.thm.fps.xneq.props.e.ass} \end{equation}
59

Then, we have

\begin{align} & \sum _{s\in S}a_{s}\overset {x^{n}}{\equiv }\sum _{s\in S}b_{s} ;\label{eq.thm.fps.xneq.props.e.+}\\ & \prod _{s\in S}a_{s}\overset {x^{n}}{\equiv }\prod _{s\in S}b_{s}. \label{eq.thm.fps.xneq.props.e.*} \end{align}
theorem PowerSeries.XnEquiv.add {R : Type u_1} [CommSemiring R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) :
a + c ≡[x^n] b + d
theorem PowerSeries.XnEquiv.sub {R : Type u_2} [CommRing R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) :
a - c ≡[x^n] b - d
theorem PowerSeries.XnEquiv.mul {R : Type u_1} [CommSemiring R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) :
a * c ≡[x^n] b * d
theorem PowerSeries.XnEquiv.smul {R : Type u_1} [CommSemiring R] {n : ℕ} {a b : PowerSeries R} (hab : a ≡[x^n] b) (r : R) :
r • a ≡[x^n] r • b
theorem PowerSeries.XnEquiv.invOfUnit {R : Type u_2} [CommRing R] {n : ℕ} {a b : PowerSeries R} (ua ub : Rˣ) (ha : constantCoeff a = ↑ua) (hb : constantCoeff b = ↑ub) (hab : a ≡[x^n] b) :
theorem PowerSeries.XnEquiv.inv {K : Type u_2} [Field K] {n : ℕ} {a b : PowerSeries K} (ha : constantCoeff a ≠ 0) (hb : constantCoeff b ≠ 0) (hab : a ≡[x^n] b) :
theorem PowerSeries.XnEquiv.div {R : Type u_2} [CommRing R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (u : Rˣ) (hu : constantCoeff c = ↑u) (v : Rˣ) (hv : constantCoeff d = ↑v) :
theorem PowerSeries.XnEquiv.sum {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] {n : ℕ} {s : Finset ι} {a b : ι → PowerSeries R} (h : ∀ i ∈ s, a i ≡[x^n] b i) :
∑ i ∈ s, a i ≡[x^n] ∑ i ∈ s, b i
theorem PowerSeries.XnEquiv.prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} [DecidableEq ι] {n : ℕ} {s : Finset ι} {a b : ι → PowerSeries R} (h : ∀ i ∈ s, a i ≡[x^n] b i) :
∏ i ∈ s, a i ≡[x^n] ∏ i ∈ s, b i
Proof ▶

All of these properties are analogous to familiar properties of integer congruences, except for Theorem 1.328 (d), which is moot for integers (since there are not many integers that are invertible in \(\mathbb {Z}\)).

(a) Reflexivity, symmetry and transitivity follow directly from the corresponding properties of equality of coefficients.

(b) For addition: If \(a\overset {x^{n}}{\equiv }b\) and \(c\overset {x^{n}}{\equiv }d\), then for each \(m\in \{ 0,1,\ldots ,n\} \) we have \([x^m](a+c)=[x^m]a+[x^m]c=[x^m]b+[x^m]d=[x^m](b+d)\). Subtraction is analogous.

For multiplication: We have \([x^m](ac)=\sum _{i=0}^{m}[x^i]a\cdot [x^{m-i}]c\). Since \(m\leq n\), each \(i\leq m\) satisfies \(i\leq n\) and \(m-i\leq n\), so \([x^i]a=[x^i]b\) and \([x^{m-i}]c=[x^{m-i}]d\). Thus \([x^m](ac)=[x^m](bd)\).

(c) For each \(m\leq n\), we have \([x^m](\lambda a)=\lambda \cdot [x^m]a=\lambda \cdot [x^m]b=[x^m](\lambda b)\).

(d) Let \(a,b\in K[[x]]\) be two invertible FPSs satisfying \(a\overset {x^{n}}{\equiv }b\). We want to show that \(a^{-1}\overset {x^{n}}{\equiv }b^{-1}\).

The FPS \(a\) is invertible; thus, its constant term \([x^{0}]a\) is invertible in \(K\) (by Proposition 1.111).

We prove that each \(m\in \{ 0,1,\ldots ,n\} \) satisfies \([x^{m}](a^{-1})=[x^{m}](b^{-1})\) by strong induction on \(m\). Fix some \(k\in \{ 0,1,\ldots ,n\} \), and assume (as induction hypothesis) that \([x^{m}](a^{-1})=[x^{m}](b^{-1})\) for each \(m\in \{ 0,1,\ldots ,k-1\} \).

We know that

\begin{align*} [x^{k}](aa^{-1}) & =\sum _{i=0}^{k}[x^{i}]a\cdot [x^{k-i}](a^{-1})\\ & =[x^{0}]a\cdot [x^{k}](a^{-1})+\sum _{i=1}^{k}[x^{i}]a\cdot [x^{k-i}](a^{-1}) \end{align*}

(here, we have split off the addend for \(i=0\) from the sum). Thus,

\[ [x^{0}]a\cdot [x^{k}](a^{-1})+\sum _{i=1}^{k}[x^{i}]a\cdot [x^{k-i}](a^{-1})=[x^{k}]\underbrace{(aa^{-1})}_{=1}=[x^{k}]1. \]

We can solve this equation for \([x^{k}](a^{-1})\) (since \([x^{0}]a\) is invertible), and thus obtain

\[ [x^{k}](a^{-1})=\frac{1}{[x^{0}]a}\cdot \left([x^{k}]1-\sum _{i=1}^{k} [x^{i}]a\cdot [x^{k-i}](a^{-1})\right). \]

The same argument (applied to \(b\) instead of \(a\)) yields

\[ [x^{k}](b^{-1})=\frac{1}{[x^{0}]b}\cdot \left([x^{k}]1-\sum _{i=1}^{k} [x^{i}]b\cdot [x^{k-i}](b^{-1})\right). \]

The right hand sides of the latter two equalities are equal (since each \(i\in \{ 1,2,\ldots ,k\} \) satisfies \([x^{i}]a=[x^{i}]b\) as a consequence of \(a\overset {x^{n}}{\equiv }b\), and satisfies \([x^{k-i}](a^{-1})=[x^{k-i}](b^{-1})\) as a consequence of the induction hypothesis, and since we have \([x^{0}]a=[x^{0}]b\) as a consequence of \(a\overset {x^{n}}{\equiv }b\)). Hence, the left hand sides must also be equal. In other words, \([x^{k}](a^{-1})=[x^{k}](b^{-1})\), which is precisely what we wanted to prove. Thus, the induction step is complete, so that \(a^{-1}\overset {x^{n}}{\equiv }b^{-1}\) is proved.

(e) Combine parts (b) and (d): we have \(a\overset {x^{n}}{\equiv }b\) and \(c^{-1}\overset {x^{n}}{\equiv }d^{-1}\) (by (d)), so \(ac^{-1}\overset {x^{n}}{\equiv }bd^{-1}\) (by (b)).

(f) The sum case follows by induction on \(|S|\) using part (b) for the induction step (adding one element at a time). The product case is analogous, using the multiplication part of (b).

Lemma 1.329
✓

Let \(n\in \mathbb {N}\). If \(a,b\in K[[x]]\) satisfy \(a\overset {x^{n}}{\equiv }b\), then \(-a\overset {x^{n}}{\equiv }-b\).

theorem PowerSeries.XnEquiv.neg {R : Type u_2} [CommRing R] {n : ℕ} {a b : PowerSeries R} (hab : a ≡[x^n] b) :
Proof ▶

For each \(m\leq n\), we have \([x^m](-a)=-[x^m]a=-[x^m]b=[x^m](-b)\).

1.11.2 Helpers for inversion and division

Lemma 1.330
✓

Let \(n\in \mathbb {N}\). Let \(f,g\in K[[x]]\) be two FPSs satisfying \(f\overset {x^{n}}{\equiv }g\), and let \(u,v\) be units of \(K\) satisfying \(u = v\). Then the FPS obtained by inverting \(f\) using the unit \(u\) is \(x^n\)-equivalent to the FPS obtained by inverting \(g\) using the unit \(v\).

theorem PowerSeries.XnEquiv.invOfUnit' {R : Type u_2} [CommRing R] {n : ℕ} {f g : PowerSeries R} (u v : Rˣ) (huv : ↑u = ↑v) (hfg : f ≡[x^n] g) :
Proof ▶

The proof proceeds by strong induction on the coefficient index, analogous to the proof of Theorem 1.328 (d), using the equality of unit values \(u=v\) and the \(x^n\)-equivalence of \(f\) and \(g\).

Lemma 1.331
✓

Let \(n\in \mathbb {N}\). Let \(a,b,c,d\in K[[x]]\) be four FPSs satisfying \(a\overset {x^{n}}{\equiv }b\) and \(c\overset {x^{n}}{\equiv }d\), and let \(c\) and \(d\) have invertible constant terms. Then \(a \cdot c^{-1}\overset {x^{n}}{\equiv }b \cdot d^{-1}\).

theorem PowerSeries.XnEquiv.div {R : Type u_2} [CommRing R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (u : Rˣ) (hu : constantCoeff c = ↑u) (v : Rˣ) (hv : constantCoeff d = ↑v) :
Proof ▶

The constant terms of \(c\) and \(d\) agree (since \(c\overset {x^{n}}{\equiv }d\)), so Lemma 1.330 gives \(c^{-1}\overset {x^{n}}{\equiv }d^{-1}\). Then \(a \cdot c^{-1}\overset {x^{n}}{\equiv }b \cdot d^{-1}\) by the multiplication rule of Theorem 1.328 (b).

Lemma 1.332
✓

Let \(n\in \mathbb {N}\). If \(a,b\in K[[x]]\) satisfy \(a\overset {x^{n}}{\equiv }b\), then \(a^k\overset {x^{n}}{\equiv }b^k\) for every \(k\in \mathbb {N}\).

theorem PowerSeries.XnEquiv.pow {R : Type u_1} [CommSemiring R] {n : ℕ} {a b : PowerSeries R} (hab : a ≡[x^n] b) (k : ℕ) :
a ^ k ≡[x^n] b ^ k
Proof ▶

By induction on \(k\). The base case \(k=0\) gives \(a^0=1=b^0\), which is trivially \(x^n\)-equivalent to itself. For the induction step, \(a^{k+1}=a^k\cdot a \overset {x^{n}}{\equiv }b^k\cdot b=b^{k+1}\) by the induction hypothesis and (57).

Lemma 1.333
✓

Let \(n\in \mathbb {N}\). Two FPSs \(f,g\in K[[x]]\) satisfy \(f\overset {x^{n}}{\equiv }g\) if and only if \(\operatorname {trunc}_{n+1}(f)=\operatorname {trunc}_{n+1}(g)\).

theorem PowerSeries.xnEquiv_iff_trunc {R : Type u_1} [CommSemiring R] {n : ℕ} {f g : PowerSeries R} :
(f ≡[x^n] g) ↔ (trunc (n + 1)) f = (trunc (n + 1)) g
Proof ▶

The truncation \(\operatorname {trunc}_{n+1}(f)\) is the polynomial \(\sum _{k=0}^{n}([x^k]f)\cdot x^k\). Two such truncations are equal if and only if all their coefficients at degrees \(0,1,\ldots ,n\) agree, which is exactly the condition \(f\overset {x^{n}}{\equiv }g\).

Lemma 1.334
✓

Let \(n\in \mathbb {N}\) and \(f\in K[[x]]\). There exists a polynomial \(p\in K[x]\) such that \(f\overset {x^{n}}{\equiv }p\).

theorem PowerSeries.exists_polynomial_xnEquiv {R : Type u_1} [CommSemiring R] (n : ℕ) (f : PowerSeries R) :
∃ (p : Polynomial R), f ≡[x^n] ↑p
Proof ▶

Take \(p=\sum _{k=0}^{n}([x^k]f)\cdot x^k\). Then for each \(m\leq n\), \([x^m]p=[x^m]f\).

1.11.3 Divisibility characterization

Proposition 1.335
✓

Let \(n\in \mathbb {N}\). Let \(f,g\in K\left[\left[x\right]\right]\) be two FPSs. Then, we have \(f\overset {x^{n}}{\equiv }g\) if and only if the FPS \(f-g\) is a multiple of \(x^{n+1}\).

theorem PowerSeries.xnEquiv_iff_dvd {R : Type u_3} [CommRing R] {n : ℕ} {f g : PowerSeries R} :
(f ≡[x^n] g) ↔ X ^ (n + 1) ∣ f - g
Proof ▶

A simple consequence of Lemma 1.130.

\((\Longrightarrow )\): Assume \(f\overset {x^{n}}{\equiv }g\). Then for each \(m{\lt}n+1\) (i.e., \(m\leq n\)), we have \([x^m](f-g)=[x^m]f-[x^m]g=0\). Thus the first \(n+1\) coefficients of \(f-g\) are \(0\), so \(f-g\) is a multiple of \(x^{n+1}\) by Lemma 1.130.

\((\Longleftarrow )\): Assume \(x^{n+1}\mid (f-g)\). Then for each \(m{\lt}n+1\), we have \([x^m](f-g)=0\) (by the power series analogue of Lemma 1.130), so \([x^m]f=[x^m]g\). Since this holds for each \(m\leq n\), we obtain \(f\overset {x^{n}}{\equiv }g\).

Lemma 1.336
✓

Let \(n\in \mathbb {N}\). Let \(f,g\in K[[x]]\) be two FPSs. Then, \(f\overset {x^{n}}{\equiv }g\) if and only if there exists a \(q\in K[[x]]\) such that \(f-g=x^{n+1}q\).

theorem PowerSeries.xnEquiv_iff_sub_eq_mul_X_pow {R : Type u_3} [CommRing R] {n : ℕ} {f g : PowerSeries R} :
(f ≡[x^n] g) ↔ ∃ (q : PowerSeries R), f - g = X ^ (n + 1) * q
Proof ▶

This is simply a restatement of Proposition 1.335, since “\(f-g\) is a multiple of \(x^{n+1}\)” means exactly that there exists such a \(q\).

1.11.4 Composition

Lemma 1.337
✓

Let \(f\in K[[x]]\) be an FPS with \([x^0]f=0\). Let \(m,k\in \mathbb {N}\) with \(m{\lt}k\). Then \([x^m](f^k)=0\).

theorem PowerSeries.coeff_pow_eq_zero_of_lt_of_constantCoeff_eq_zero {R : Type u_3} [CommRing R] {f : PowerSeries R} (hf : constantCoeff f = 0) {m k : ℕ} (hmk : m < k) :
(coeff m) (f ^ k) = 0
Proof ▶

Since \([x^0]f=0\), the order of \(f\) is at least \(1\), and thus the order of \(f^k\) is at least \(k{\gt}m\). Hence \([x^m](f^k)=0\).

Proposition 1.338

Let \(n\in \mathbb {N}\). Let \(a,b,c,d\in K\left[\left[x\right]\right]\) be four FPSs satisfying \(a\overset {x^{n}}{\equiv }b\) and \(c\overset {x^{n}}{\equiv }d\) and \([x^{0}]c=0\) and \([x^{0}]d=0\). Then,

\[ a\circ c\overset {x^{n}}{\equiv }b\circ d. \]
theorem PowerSeries.XnEquiv.comp {R : Type u_3} [CommRing R] {n : ℕ} {a b c d : PowerSeries R} (hab : a ≡[x^n] b) (hcd : c ≡[x^n] d) (hc : constantCoeff c = 0) (hd : constantCoeff d = 0) :
Proof ▶

Write \(a\) and \(b\) as \(a=\sum _{i\in \mathbb {N}}a_{i}x^{i}\) and \(b=\sum _{i\in \mathbb {N}}b_{i}x^{i}\) (with \(a_{i},b_{i}\in K\)). Then, \(a\overset {x^{n}}{\equiv }b\) means that \(a_{i}=b_{i}\) for all \(i\leq n\). Combine this with \(c^{i}\overset {x^{n}}{\equiv }d^{i}\) (which holds for all \(i\in \mathbb {N}\) as a consequence of \(c\overset {x^{n}}{\equiv }d\) and of (61)) to obtain the relation \(a_{i}c^{i}\overset {x^{n}}{\equiv }b_{i}d^{i}\) for all \(i\leq n\). But this relation also holds for all \(i{\gt}n\), since all such \(i\) satisfy \([x^{m}](c^{i})=[x^{m}](d^{i})=0\) for all \(m\in \{ 0,1,\ldots ,n\} \) (a consequence of Lemma 1.337 using \([x^{0}]c=0\) and \([x^{0}]d=0\)). Thus, the relation \(a_{i}c^{i}\overset {x^{n}}{\equiv }b_{i}d^{i}\) holds for all \(i\in \mathbb {N}\). Summing over all \(i\), we find \(a\circ c\overset {x^{n}}{\equiv }b\circ d\).

1.11.5 Equality via \(x^n\)-equivalence

Lemma 1.339
✓

Two FPSs \(f,g\in K[[x]]\) are equal if and only if \(f\overset {x^{n}}{\equiv }g\) for all \(n\in \mathbb {N}\).

theorem PowerSeries.eq_iff_forall_xnEquiv {R : Type u_1} [CommSemiring R] {f g : PowerSeries R} :
f = g ↔ ∀ (n : ℕ), f ≡[x^n] g
Proof ▶

\((\Longrightarrow )\): If \(f=g\), then \(f\overset {x^{n}}{\equiv }g\) for every \(n\) by reflexivity.

\((\Longleftarrow )\): If \(f\overset {x^{n}}{\equiv }g\) for all \(n\), then in particular for each \(m\in \mathbb {N}\), taking \(n=m\) gives \([x^m]f=[x^m]g\) (since \(m\leq m\)). Thus \(f=g\) by extensionality (Lemma 1.86).