Dependencies

Let \(A\) be a weighted set. Then, \(A^{k}\) (for \(k\in \mathbb {N}\)) means the weighted set \(\underbrace{A\times A\times \cdots \times A}_{k\text{ times}}\).

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

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

This is not obvious from the formula when \(n\) is odd, since the summands can be negative.

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) and \(d_1, d_2, \ldots , d_n \in K\). Then,

and

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) and \(\tau \in S_n\). Then,

and

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

For any \(c\in K\) and \(k\in \mathbb {N}\),

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\).

Each FPS is a limit of a sequence of polynomials. Indeed, if \(a=\sum _{n\in \mathbb {N}}a_{n}x^{n}\) (with \(a_{n}\in K\)), then

More precisely, the sequence of truncations \((\operatorname {trunc}_{i+1}(a))_{i \in \mathbb {N}}\) coefficientwise stabilizes to \(a\).

Let \(k\in \mathbb {N}\). For each \(i\in \left\{ 1,2,\ldots ,k\right\} \), let \(f_{i}\) be an FPS, and let \(\left( f_{i,n}\right) _{n\in \mathbb {N}}\) be a sequence of FPSs such that

(note that it is \(n\), not \(i\), that goes to \(\infty \) here!). Then,

Let \(f\) be any FPS in \(K\left[\left[x\right] \right]_{1}\). Then, \(\operatorname {loder}\left(f^{-1}\right) =-\operatorname {loder}f\).

(Here, we do not use Convention 1.210; thus, \(K\) can be an arbitrary commutative ring.)

Let \(f_{1},f_{2},\ldots ,f_{k}\) be any \(k\) FPSs in \(K\left[\left[x\right]\right]_{1}\). Then,

(Here, we do not use Convention 1.210; thus, \(K\) can be an arbitrary commutative ring.)

Any FPS \(\left(a_{0},a_{1},a_{2},\ldots \right) \in K\left[\left[x\right]\right]\) satisfies

In particular, the right hand side here is well-defined, i.e., the family \(\left(a_{n}x^{n}\right)_{n\in \mathbb {N}}\) is summable.

Let \(k \in \mathbb {N}\). Let \(a_1, a_2, \ldots , a_k\) and \(b_1, b_2, \ldots , b_k\) be nonnegative integers such that

Then,

Let \(n,k\in \mathbb {N}\). Then, \(\binom {n}{k}^{2}\geq \binom {n}{k-1}\cdot \binom {n}{k+1}\).

Let \(k \in \mathbb {N}\). Recall the Catalan numbers \(c_n = \frac{1}{n+1}\binom {2n}{n}\) for all \(n \in \mathbb {N}\). Then,

Consider the setting of Theorem 5.154, but additionally assume that

Here, \(\operatorname {x}(P)\) and \(\operatorname {y}(P)\) denote the two coordinates of any point \(P \in \mathbb {Z}^2\).

Then, there are no nipats from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\) when \(\sigma \in S_k\) is not the identity permutation \(\operatorname {id} \in S_k\). Therefore, the claim of Theorem 5.154 simplifies to

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

For each positive integer \(n\), we have

Let \(n \in \mathbb {N}\). The set of all even permutations in \(S_n\) is a normal subgroup of \(S_n\).

Let \(n \in \mathbb {N}\). Then, the group \(S_n\) is generated by the simples \(s_0, s_1, \ldots , s_{n-2}\).

Let \(n \geq 2\). Then,

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

(a) We have \(\ell (\sigma \tau ) \equiv \ell (\sigma ) + \ell (\tau ) \pmod{2}\) for all \(\sigma , \tau \in S_n\).

(b) We have \(\ell (\sigma \tau ) \leq \ell (\sigma ) + \ell (\tau )\) for all \(\sigma , \tau \in S_n\).

(c) Let \(k_1, k_2, \ldots , k_q \in [n-1]\), and let \(\sigma = s_{k_1} s_{k_2} \cdots s_{k_q}\). Then \(q \geq \ell (\sigma )\) and \(q \equiv \ell (\sigma ) \pmod{2}\).

Part (a) of Corollary 3.85: The length of a product has the same parity as the sum of lengths.

Part (b) of Corollary 3.85: The triangle inequality \(\ell (\sigma \tau ) \leq \ell (\sigma ) + \ell (\tau )\).

Part (c) of Corollary 3.85: For any word representing \(\sigma \), the word length is at least \(\ell (\sigma )\) and has the same parity as \(\ell (\sigma )\).

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

is a group homomorphism from the symmetric group \(S_n\) to the order-\(2\) group \(\{ 1, -1\} \). (Of course, \(\{ 1, -1\} \) is a group with respect to multiplication.)

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

(a) We have \(\sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^m = 0\) for any \(m \in \mathbb {N}\) satisfying \(m {\lt} n\).

(b) We have \(\sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^n = n!\).

(c) We have \(\sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^m \geq 0\) for each \(m \in \mathbb {N}\).

(d) We have \(n! \mid \sum _{k=0}^{n} (-1)^k \binom {n}{k} (n-k)^m\) for each \(m \in \mathbb {N}\).

The acceptable sets for parameters \(n, m \in \mathbb {N}\) are the subsets of \(\{ 0, 1, \ldots , n-1\} \) with cardinality at most \(m\):

A commutative ring means a set \(K\) equipped with three maps

and two elements \(\mathbf{0}\in K\) and \(\mathbf{1}\in K\) satisfying the following axioms:

1. Commutativity of addition: We have \(a\oplus b=b\oplus a\) for all \(a,b\in K\).

2. Associativity of addition: We have \(a\oplus \left( b\oplus c\right) =\left( a\oplus b\right) \oplus c\) for all \(a,b,c\in K\).

3. Neutrality of zero: We have \(a\oplus \mathbf{0}=\mathbf{0}\oplus a=a\) for all \(a\in K\).

4. Subtraction undoes addition: Let \(a,b,c\in K\). We have \(a\oplus b=c\) if and only if \(a=c\ominus b\).

5. Commutativity of multiplication: We have \(a\odot b=b\odot a\) for all \(a,b\in K\).

6. Associativity of multiplication: We have \(a\odot \left( b\odot c\right) =\left( a\odot b\right) \odot c\) for all \(a,b,c\in K\).

7. Distributivity: We have

   \[ a\odot \left( b\oplus c\right) =\left( a\odot b\right) \oplus \left( a\odot c\right) \ \ \ \ \ \ \ \ \ \ \text{and}\ \ \ \ \ \ \ \ \ \ \left( a\oplus b\right) \odot c=\left( a\odot c\right) \oplus \left( b\odot c\right) \]

   for all \(a,b,c\in K\).

8. Neutrality of one: We have \(a\odot \mathbf{1}=\mathbf{1}\odot a=a\) for all \(a\in K\).

9. Annihilation: We have \(a\odot \mathbf{0}=\mathbf{0}\odot a=\mathbf{0}\) for all \(a\in K\).

The operations \(\oplus \), \(\ominus \) and \(\odot \) are called the addition, the subtraction and the multiplication of the ring \(K\). When confusion is unlikely, we will denote these three operations \(\oplus \), \(\ominus \) and \(\odot \) by \(+\), \(-\) and \(\cdot \), respectively, and we will abbreviate \(a\odot b=a\cdot b\) by \(ab\).

The elements \(\mathbf{0}\) and \(\mathbf{1}\) are called the zero and the unity (or the one) of the ring \(K\). We will simply call these elements \(0\) and \(1\) when confusion with the corresponding numbers is unlikely.

We will use PEMDAS conventions for the three operations \(\oplus \), \(\ominus \) and \(\odot \). These imply that the operation \(\odot \) has higher precedence than \(\oplus \) and \(\ominus \), while the operations \(\oplus \) and \(\ominus \) are left-associative.

A \(K\)-algebra is a set \(A\) equipped with four maps

and two elements \(\overrightarrow {0}\in A\) and \(\overrightarrow {1}\in A\) satisfying the following properties:

1. The set \(A\), equipped with the maps \(\oplus \), \(\ominus \) and \(\odot \) and the two elements \(\overrightarrow {0}\) and \(\overrightarrow {1}\), is a (noncommutative) ring.

2. The set \(A\), equipped with the maps \(\oplus \), \(\ominus \) and \(\rightharpoonup \) and the element \(\overrightarrow {0}\), is a \(K\)-module.

3. We have

   \begin{equation} \lambda \rightharpoonup \left( a\odot b\right) =\left( \lambda \rightharpoonup a\right) \odot b=a\odot \left( \lambda \rightharpoonup b\right) \label{eq.def.alg.Kalg.scaleinv}\end{equation}

   14

   for all \(\lambda \in K\) and \(a,b\in A\).

(Thus, in a nutshell, a \(K\)-algebra is a set \(A\) that is simultaneously a ring and a \(K\)-module, with the property that the ring \(A\) and the \(K\)-module \(A\) have the same addition, the same subtraction and the same zero, and satisfy the additional compatibility property (14).)

Let \(K\) be a commutative ring.

A \(K\)-module means a set \(M\) equipped with three maps

(notice that the third map has domain \(K\times M\), not \(M\times M\)) and an element \(\overrightarrow {0}\in M\) satisfying the following axioms:

1. Commutativity of addition: We have \(a\oplus b=b\oplus a\) for all \(a,b\in M\).

2. Associativity of addition: We have \(a\oplus \left( b\oplus c\right) =\left( a\oplus b\right) \oplus c\) for all \(a,b,c\in M\).

3. Neutrality of zero: We have \(a\oplus \overrightarrow {0}=\overrightarrow {0}\oplus a=a\) for all \(a\in M\).

4. Subtraction undoes addition: Let \(a,b,c\in M\). We have \(a\oplus b=c\) if and only if \(a=c\ominus b\).

5. Associativity of scaling: We have \(u\rightharpoonup \left( v\rightharpoonup a\right) =\left( uv\right) \rightharpoonup a\) for all \(u,v\in K\) and \(a\in M\).

6. Left distributivity: We have \(u\rightharpoonup \left( a\oplus b\right) =\left( u\rightharpoonup a\right) \oplus \left( u\rightharpoonup b\right) \) for all \(u\in K\) and \(a,b\in M\).

7. Right distributivity: We have \(\left( u+v\right) \rightharpoonup a=\left( u\rightharpoonup a\right) \oplus \left( v\rightharpoonup a\right) \) for all \(u,v\in K\) and \(a\in M\).

8. Neutrality of one: We have \(1\rightharpoonup a=a\) for all \(a\in M\).

9. Left annihilation: We have \(0\rightharpoonup a=\overrightarrow {0}\) for all \(a\in M\).

10. Right annihilation: We have \(u\rightharpoonup \overrightarrow {0}=\overrightarrow {0}\) for all \(u\in K\).

The operations \(\oplus \), \(\ominus \) and \(\rightharpoonup \) are called the addition, the subtraction and the scaling (or the \(K\)-action) of the \(K\)-module \(M\). When confusion is unlikely, we will denote these three operations \(\oplus \), \(\ominus \) and \(\rightharpoonup \) by \(+\), \(-\) and \(\cdot \), respectively, and we will abbreviate \(a\rightharpoonup b=a\cdot b\) by \(ab\).

The element \(\overrightarrow {0}\) is called the zero (or the zero vector) of the \(K\)-module \(M\). We will usually just call it \(0\).

When \(M\) is a \(K\)-module, the elements of \(M\) are called vectors, while the elements of \(K\) are called scalars.

We will use PEMDAS conventions for the three operations \(\oplus \), \(\ominus \) and \(\rightharpoonup \), with the operation \(\rightharpoonup \) having higher precedence than \(\oplus \) and \(\ominus \).

The notion of a ring (also known as a noncommutative ring) is defined in the exact same way as we defined the notion of a commutative ring in Definition 1.42, except that the “Commutativity of multiplication” axiom is removed.

For any numbers \(n\) and \(k\), we set

Note that “numbers” is to be understood fairly liberally here. In particular, \(n\) can be any integer, rational, real or complex number (or, more generally, any element in a \(\mathbb {Q}\)-algebra), whereas \(k\) can be anything (although the only nonzero values of \(\binom {n}{k}\) will be achieved for \(k\in \mathbb {N}\), by the above definition).

The set of \(d\)-blocky \(k\)-element subsets of \(\{ 0, \ldots , n-1\} \):

Let \(n\in \mathbb {N}\) and \(d\in \mathbb {N}\). An \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\) is said to be all-even if each element of \(\left[ d\right] \) occurs an even number of times in this \(n\)-tuple (i.e., if for each \(k\in \left[ d\right] \), the number of all \(i\in \left[ n\right] \) satisfying \(x_{i}=k\) is even).

The set of all-even \(n\)-tuples in \([d]^n\) is

For \(k \in [d]\), the map \(\operatorname {flipSign}_k : \{ 1,-1\} ^d \to \{ 1,-1\} ^d\) sends a \(d\)-tuple \((e_1, \ldots , e_d)\) to the tuple obtained by flipping the sign of the \(k\)-th entry: i.e., replacing \(e_k\) by \(-e_k\) and leaving all other entries unchanged.

For an \(n\)-tuple \(x : \operatorname {Fin} n \to \operatorname {Fin} d\) and \(k \in \operatorname {Fin} d\), the multiplicity of \(k\) in \(x\) is the number of all \(i \in \operatorname {Fin} n\) satisfying \(x(i) = k\).

For a sign tuple \(e : \operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}\) and an index tuple \(x : \operatorname {Fin} n \to \operatorname {Fin} d\), the sign product is

For a sign tuple \(e : \operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}\), the sign sum is the integer

The map \(\operatorname {signTupleToSubset} : (\operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z}) \to \mathcal{P}(\operatorname {Fin} d)\) sends a sign tuple \(e\) to the set \(S = \{ k \in \operatorname {Fin} d \mid e_k = 1\} \) (i.e., the positions where \(\operatorname {toSign}(e_k) = -1\)).

The inverse map \(\operatorname {subsetToSignTuple} : \mathcal{P}(\operatorname {Fin} d) \to (\operatorname {Fin} d \to \mathbb {Z}/2\mathbb {Z})\) sends a subset \(S \subseteq \operatorname {Fin} d\) to the sign tuple where position \(k\) has value \(1\) (representing \(-1\)) if \(k \in S\), and \(0\) (representing \(+1\)) otherwise.

The function \(\operatorname {toSign} : \mathbb {Z}/2\mathbb {Z} \to \mathbb {Z}\) converts elements of \(\mathbb {Z}/2\mathbb {Z}\) to signs: \(\operatorname {toSign}(0) = 1\) and \(\operatorname {toSign}(1) = -1\).

The \(n\)-th Catalan number is \(c_n = \frac{1}{n+1}\binom {2n}{n}\).

A Dyck word of length \(2n\) is a list of \(0\)s and \(1\)s with equal numbers of each, such that every prefix has at least as many \(1\)s as \(0\)s.

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}\).

For an invertible element \(a\) and any \(b \in L\), the fraction \(b/a\) is defined as \(b \cdot a^{-1}\).

Let \(L\) be a commutative ring and \(a, b \in L\).

(a) We say that \(b\) is an inverse (or multiplicative inverse) of \(a\) if \(a \cdot b = 1\).

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

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.

An element \(a \in L\) is invertible if there exists \(b \in L\) such that \(a \cdot b = 1\).

Given \(P,Q\subseteq [n]\) with \(|P|=|Q|\) and permutations \(\alpha \in S_k\), \(\beta \in S_\ell \) (with \(k=|P|\), \(\ell =|\overline{P}|\)), define \(\sigma \in S_n\) by:

This is the inverse of the map \(\sigma \mapsto (\alpha _\sigma ,\beta _\sigma )\).

Let \(L\) be a commutative ring. Let \(a\in L\). The element \(a\) of \(L\) is said to be regular if and only if every \(x\in L\) satisfying \(ax=0\) satisfies \(x=0\).

The cycle lengths of \(\sigma \) is the multiset of lengths of the nontrivial cycles (length \(\geq 2\)) in the cycle decomposition of \(\sigma \).

Let \(c\) be a cycle permutation (i.e., \(c\) is a cycle in the sense of Definition 3.124). The minimum element of \(c\) is the smallest element in the support of \(c\).

Let \(c\) be a cycle permutation. The canonical list representation of \(c\) is the list \((a, c(a), c^2(a), \ldots )\) where \(a\) is the minimum element of \(c\) (Definition 3.141).

Given a list of lists (each representing a cycle), the corresponding permutation is obtained by composing the cycle permutations \(\operatorname {cyc}_{a_1, a_2, \ldots , a_m}\) for each list \((a_1, a_2, \ldots , a_m)\) in the input.

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) be an \(n \times n\)-matrix. We define a new \(n \times n\)-matrix \(\operatorname {adj} A \in K^{n \times n}\) by

This matrix \(\operatorname {adj} A\) is called the adjugate (or classical adjoint) of the matrix \(A\). Note the index swap: the \((i,j)\) entry involves removing row \(j\) and column \(i\).

The formalization shows that this definition equals Mathlib’s Matrix.adjugate, which is defined via \((\operatorname {adj} A)_{i,j} = \det (A')\) where \(A'\) is the matrix \(A\) with row \(j\) replaced by the \(i\)-th standard basis vector.

Let \(n \in \mathbb {N}\). Let \(A \in K^{n \times n}\) be an \(n \times n\)-matrix. The determinant \(\det A\) of \(A\) is defined to be the element

of \(K\). Here:

• we let \(S_n\) denote the \(n\)-th symmetric group (i.e., the group of permutations of \([n] = \{ 1, 2, \ldots , n\} \));

• we let \((-1)^{\sigma }\) denote the sign of the permutation \(\sigma \) (as defined in Definition 3.109).

The image of a finite subset \(P \subseteq [n]\) under a permutation \(\sigma \in S_n\) is \(\sigma (P) = \{ \sigma (i) \mid i \in P\} \).

The set of permutations mapping \(P\) to \(Q\): \(\mathrm{permsMapping}(P, Q) = \{ \sigma \in S_n \mid \sigma (P) = Q\} \).

Given a subset \(P\) of \([m]\), the sorting equivalence is a bijection

that sends the \(i\)-th element of the left component to the \(i\)-th smallest element of \(P\) and the \(j\)-th element of the right component to the \(j\)-th smallest element of \(P^c\). This equivalence is used to decompose matrices into block form with respect to the partition \([m] = P \sqcup P^c\).

Let \(n,m\in \mathbb {N}\). Let \(A\) be an \(n\times m\)-matrix.

Let \(U\) be a subset of \([n]\). Let \(V\) be a subset of \([m]\).

Writing the two sets \(U\) and \(V\) as

with

we set

Roughly speaking, \(\operatorname {sub}_U^V A\) is the matrix obtained from \(A\) by focusing only on the \(i\)-th rows for \(i\in U\) (that is, removing all the other rows) and only on the \(j\)-th columns for \(j\in V\) (that is, removing all the other columns).

This matrix \(\operatorname {sub}_U^V A\) is called the submatrix of \(A\) obtained by restricting to the \(U\)-rows and the \(V\)-columns. If this matrix is square (i.e., if \(|U|=|V|\)), then its determinant \(\det (\operatorname {sub}_U^V A)\) is called a minor of \(A\).

The submatrix determinant of an \(n \times n\) matrix \(A\) with row set \(P\) and column set \(Q\) (both subsets of \([n]\)) is

where \(A[P, Q]\) is the submatrix of \(A\) with rows indexed by \(P\) and columns indexed by \(Q\), in the order determined by their natural ordering.

The variable substitution \(\varphi _{i \to j}\) is the algebra homomorphism \(R[x_1, \ldots , x_n] \to R[x_1, \ldots , x_n]\) that sends \(x_i \mapsto x_j\) and fixes all other variables.

(a) There is a conversion from natural-number-based dominos (with natural number coordinates) to integer-based dominos (with integer coordinates) given by casting each coordinate.

(b) There is a conversion from integer-based dominos with positive coordinates back to natural-number-based dominos.

(c) There is a conversion from natural-number-based tilings of \(R_{n,m}\) to integer-based tilings of \(R_{n,m}\) obtained by converting each domino.

Given a tiling \(T\) of \(R_{n,3}\), the reflection of \(T\) is the tiling obtained by applying the cell map \((x, y) \mapsto (x, 4 - y)\) to every cell of every domino. This swaps rows \(1 \leftrightarrow 3\) and fixes row \(2\).

(a) A shape means a subset of \(\mathbb {Z}^{2}\).

We draw each \(\left( i,j\right) \in \mathbb {Z}^{2}\) as a unit square with center at the point \(\left( i,j\right) \) (in Cartesian coordinates); thus, a shape can be drawn as a cluster of squares.

(b) For any \(n,m\in \mathbb {N}\), the shape \(R_{n,m}\) (called the \(n\times m\)-rectangle) is defined to be

(c) A domino means a size-\(2\) shape of the form

for some \(\left( i,j\right) \in \mathbb {Z}^{2}\).

(d) A domino tiling of a shape \(S\) is a set partition of \(S\) into dominos (i.e., a set of disjoint dominos whose union is \(S\)).

(e) For any \(n,m\in \mathbb {N}\), let \(d_{n,m}\) be the # of domino tilings of \(R_{n,m}\).

Let \(P,Q\subseteq [n]\) with \(|P|=|Q|=k\) and let \(\sigma \in S_n\) satisfy \(\sigma (P) = Q\). Write the elements of \(P\) in increasing order as \(p_1 {\lt} \cdots {\lt} p_k\), of \(Q\) as \(q_1 {\lt} \cdots {\lt} q_k\), of \(\overline{P}\) as \(p'_1 {\lt} \cdots {\lt} p'_\ell \), and of \(\overline{Q}\) as \(q'_1 {\lt} \cdots {\lt} q'_\ell \).

Define \(\alpha _\sigma \in S_k\) by \(\sigma (p_i) = q_{\alpha _\sigma (i)}\) and \(\beta _\sigma \in S_\ell \) by \(\sigma (p'_i) = q'_{\beta _\sigma (i)}\).

The Fibonacci sequence \((f_0, f_1, f_2, \ldots )\) is defined by \(f_0 = 0\), \(f_1 = 1\), and \(f_n = f_{n-1} + f_{n-2}\) for \(n \geq 2\).

The conjugate golden ratio \(\phi _- = \frac{1-\sqrt{5}}{2}\).

The golden ratio \(\phi _+ = \frac{1+\sqrt{5}}{2}\).

For a subset \(P\subseteq [n]\), define \(\operatorname {sum}(P) = \sum _{i\in P} i\).

For subsets \(P,Q\subseteq [n]\), define \(\operatorname {Perm}(P,Q) = \{ \sigma \in S_n : \sigma (P)=Q\} \) where \(\sigma (P) = \{ \sigma (i) \mid i \in P\} \) denotes the image of \(P\) under \(\sigma \).

If \(n\in \mathbb {N}\), and if \(\mathbf{a}=\left( a_{0},a_{1},a_{2},\ldots \right) \in K\left[\left[x\right]\right]\) is an FPS, then we define an element \(\left[x^{n}\right]\mathbf{a}\in K\) by

This is called the coefficient of \(x^{n}\) in \(\mathbf{a}\), or the \(n\)-th coefficient of \(\mathbf{a}\), or the \(x^{n}\)-coefficient of \(\mathbf{a}\).

(a) An (integer) composition means a (finite) tuple of positive integers.

(b) The size of an integer composition \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{m}\right) \) is defined to be the integer \(\alpha _{1}+\alpha _{2}+\cdots +\alpha _{m}\). It is written \(\left\vert \alpha \right\vert \).

(c) The length of an integer composition \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{m}\right) \) is defined to be the integer \(m\). It is written \(\ell \left( \alpha \right) \).

(d) Let \(n\in \mathbb {N}\). A composition of \(n\) means a composition whose size is \(n\).

(e) Let \(n\in \mathbb {N}\) and \(k\in \mathbb {N}\). A composition of \(n\) into \(k\) parts is a composition whose size is \(n\) and whose length is \(k\).

Let \(f\in K\left[ \left[ x\right] \right] \) be an FPS. Then, the derivative \(f^{\prime }\) of \(f\) is an FPS defined as follows: Write \(f\) as \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\) (with \(f_{0},f_{1},f_{2},\ldots \in K\)), and set

Let \(\left(\mathbf{a}_{i}\right)_{i\in I}\in K\left[\left[x\right]\right]^{I}\) be a (possibly infinite) family of FPSs. Let \(n\in \mathbb {N}\). Let \(M\) be a finite subset of \(I\).

(a) We say that \(M\) determines the \(x^{n}\)-coefficient in the sum of \(\left(\mathbf{a}_{i}\right)_{i\in I}\) if every finite subset \(J\) of \(I\) satisfying \(M\subseteq J\subseteq I\) satisfies

(b) We say that \(M\) determines the \(x^{n}\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i\in I}\) if every finite subset \(J\) of \(I\) satisfying \(M\subseteq J\subseteq I\) satisfies

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)\).

For an essentially finite family \((a_i)_{i\in I}\), the essentially finite sum \(\sum _{i\in I} a_i\) is defined as \(\sum _{i\in S} a_i\) where \(S = \{ i\in I \mid a_i \neq 0\} \).

Define three FPS \(\exp \), \(\overline{\log }\) and \(\overline{\exp }\) in \(K\left[\left[x\right]\right]\) by

(The last equality sign here follows from \(\exp =\sum _{n\in \mathbb {N}}\frac{1}{n!}x^{n}=\underbrace{\frac{1}{0!}}_{=1}\underbrace{x^{0}}_{=1} +\sum _{n\geq 1}\frac{1}{n!}x^{n}=1+\sum _{n\geq 1}\frac{1}{n!}x^{n}\).)

(a) We let \(K\left[\left[x\right] \right]_{0}\) denote the set of all FPSs \(f\in K\left[\left[x\right] \right]\) with \(\left[x^{0}\right]f=0\).

(b) We let \(K\left[\left[x\right]\right]_{1}\) denote the set of all FPSs \(f\in K\left[\left[x\right]\right]\) with \(\left[ x^{0}\right]f=1\).

(c) We define two maps

and

(These two maps are well-defined according to parts (c) and (d) of Lemma 1.223 below.)

Define two FPSs for the binomial identity:

A formal power series (or, short, FPS) in \(1\) indeterminate over \(K\) means a sequence \(\left(a_{0},a_{1},a_{2},\ldots \right) = \left(a_{n}\right)_{n\in \mathbb {N}} \in K^{\mathbb {N}}\) of elements of \(K\).

For \(g\in K[[x]]_0\) (FPS with constant term \(0\)), we define

Since \(g\) has constant term \(0\), the substitution is well-defined.

For \(f\in K[[x]]_1\), we define

Since \(f\) has constant term \(1\), the FPS \(f-1\) has constant term \(0\), so the substitution is well-defined.

The geometric series is the FPS \(\frac{1}{1-x} = (1-x)^{-1} \in K[[x]]\) (where \(K\) is a field).

The (ordinary) generating function of a sequence \((a_0, a_1, a_2, \ldots )\) is the FPS \((a_0, a_1, a_2, \ldots ) = \sum _{n\geq 0} a_n x^n\).

An FPS \(f\in K[[x]]\) has constant term one if \([x^0]f=1\). We write \(f\in K[[x]]_1\) for this condition.

Let \(\left(\mathbf{a}_{i}\right)_{i\in I}\in K\left[\left[x\right]\right]^{I}\) be a family of FPSs. Let \(n\in \mathbb {N}\). An \(x^{n}\)-approximator for \(\left(\mathbf{a}_{i}\right)_{i\in I}\) means a finite subset \(M\) of \(I\) that determines the first \(n+1\) coefficients in the product of \(\left(\mathbf{a}_{i}\right)_{i\in I}\). (In other words, \(M\) has to determine the \(x^{m}\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i\in I}\) for each \(m\in \left\{ 0,1,\ldots ,n\right\} \).)

For a family \((p_{i,k})\) of FPSs, the coefficient support set \(T_m\) at degree \(m\) is the set \(\{ (i,k) : k \neq 0 \text{ and } [x^m] p_{i,k} \neq 0\} \).

The coefficient support union \(T'_n = T_0 \cup T_1 \cup \cdots \cup T_n\) is the union of coefficient support sets up to degree \(n\).

A family \((k_i)_{i \in I}\) of natural numbers is essentially finite if all but finitely many entries equal \(0\), i.e., the set \(\{ i \in I : k_i \neq 0\} \) is finite. This corresponds to \(S^I_{\mathrm{fin}}\) in the source.

Given a finite subset \(I_n \subseteq I\) and a function \(f : I_n \to \mathbb {N}\), extend from finset produces a function \(I \to \mathbb {N}\) by setting \(f(i)\) for \(i \in I_n\) and \(0\) otherwise. This is used in the bijection between essentially finite families supported on \(I_n\) and functions \(I_n \to S\).

The index set \(I_n\) is the set of first components appearing in \(T'_n\): \(I_n = \{ i \in I : \exists k,\; (i,k) \in T'_n\} \).

Given a finite subset \(I_n \subseteq I\) and a function \(k : I \to \mathbb {N}\), restrict to finset produces the restriction \(k|_{I_n} : I_n \to \mathbb {N}\). This is the inverse direction of the bijection used in Claim 8.

The set \(S^I_{\mathrm{fin}}\) of essentially finite families in \(\prod _{i \in I} S_i\) is the set of all families \((k_i)_{i \in I}\) such that \(k_i \in S_i\) for all \(i\) and the family \((k_i)\) is essentially finite.

The value set \(K_n\) is the set of second components appearing in \(T'_n\): \(K_n = \{ k \in \mathbb {N} : \exists i,\; (i,k) \in T'_n\} \).

A balanced ternary representation of an integer \(n\) means an essentially finite sequence \(\left( b_{i}\right) _{i\in \mathbb {N}}=\left( b_{0},b_{1},b_{2},\ldots \right) \in \left\{ 0,1,-1\right\} ^{\mathbb {N}}\) such that

A binary representation of an integer \(n\) means an essentially finite sequence \(\left( b_{i}\right) _{i\in \mathbb {N}}=\left( b_{0},b_{1},b_{2},\ldots \right) \in \left\{ 0,1\right\} ^{\mathbb {N}}\) such that

(Recall that “essentially finite” means “all but finitely many \(i\in \mathbb {N}\) satisfy \(b_{i}=0\)”.)

Let \(K\left[ \left[ x^{\pm }\right] \right] \) be the \(K\)-module \(K^{\mathbb {Z}}\) of all families \(\left( a_{n}\right) _{n\in \mathbb {Z}}=\left( \ldots ,a_{-2},a_{-1},a_{0},a_{1},a_{2},\ldots \right) \) of elements of \(K\). Its addition and its scaling are defined entrywise:

An element of \(K\left[ \left[ x^{\pm }\right] \right] \) will be called a doubly infinite power series. We use the notation \(\sum _{n\in \mathbb {Z}}a_{n}x^{n}\) for a family \(\left( a_{n}\right) _{n\in \mathbb {Z}}\in K\left[ \left[ x^{\pm }\right] \right] \).

Let \(K\left[ x^{\pm }\right] \) be the \(K\)-submodule of \(K\left[ \left[ x^{\pm }\right] \right] \) consisting of all essentially finite families \(\left( a_{n}\right) _{n\in \mathbb {Z}}\). The elements of \(K\left[ x^{\pm }\right] \) are called Laurent polynomials in the indeterminate \(x\) over \(K\).

We define a multiplication on \(K\left[ x^{\pm }\right] \) by setting

The sum \(\sum _{i\in \mathbb {Z}}a_{i}b_{n-i}\) is well-defined because it is essentially finite.

We define an element \(x\in K\left[ x^{\pm }\right] \) by

In Mathlib, Laurent polynomials are represented as finitely supported functions \(\mathbb {Z} \to K\) (the group algebra of \(\mathbb {Z}\) over \(K\)).

We let \(K\left( \left( x\right) \right) \) be the subset of \(K\left[ \left[ x^{\pm }\right] \right] \) consisting of all families \(\left( a_{i}\right) _{i\in \mathbb {Z}}\in K\left[ \left[ x^{\pm }\right] \right] \) such that the sequence \(\left( a_{-1},a_{-2},a_{-3},\ldots \right) \) is essentially finite – i.e., such that all sufficiently low \(i\in \mathbb {Z}\) satisfy \(a_{i}=0\).

The elements of \(K\left( \left( x\right) \right) \) are called Laurent series in one indeterminate \(x\) over \(K\).

In Mathlib, Laurent series are implemented as Hahn series over \(\mathbb {Z}\) with coefficients in \(K\), which are functions \(\mathbb {Z} \to K\) whose support is well-founded (equivalently, bounded below). The formalization also provides a predicate on doubly infinite power series that captures this textbook definition.

Given a Laurent series \(\mathbf{a} = (a_n)_{n \in \mathbb {Z}}\), the family of monomials \(\bigl(a_g \cdot x^g\bigr)_{g \in \operatorname {supp}(\mathbf{a})}\) forms a summable family. This construction is the key ingredient for expressing a Laurent series as a formal infinite sum of monomials.

Let \(\left( f_{i}\right) _{i\in \mathbb {N}}\in K\left[ \left[ x\right] \right] ^{\mathbb {N}}\) be a sequence of FPSs over \(K\). Let \(f\in K\left[ \left[ x\right] \right] \) be an FPS.

We say that \(\left( f_{i}\right) _{i\in \mathbb {N}}\) coefficientwise stabilizes to \(f\) if for each \(n\in \mathbb {N}\),

If \(f_{i}\) coefficientwise stabilizes to \(f\) as \(i\rightarrow \infty \), then we write \(\lim \limits _{i\rightarrow \infty }f_{i}=f\) and say that \(f\) is the limit of \(\left( f_{i}\right) _{i\in \mathbb {N}}\). This is legitimate, because \(f\) is uniquely determined by the sequence \(\left( f_{i}\right) _{i\in \mathbb {N}}\).

A family \((f_n)_{n \in \mathbb {N}}\) of FPSs is multipliable if (1) \([x^0]f_i = 1\) for all \(i\), and (2) for each \(n \in \mathbb {N}\), there exists \(N\) such that for all \(i \geq N\) and all \(k \leq n\), \([x^k]f_i = \delta _{k,0}\) (i.e., eventually all \(f_i\) are \(\equiv 1 \pmod{x^{n+1}}\)).

A family \((f_n)_{n \in \mathbb {N}}\) of FPSs is summable if for each \(n \in \mathbb {N}\), the set \(\{ i \in \mathbb {N} : [x^n] f_i \neq 0\} \) is finite.

Let \(\left( a_{i}\right) _{i\in \mathbb {N}}=\left( a_{0},a_{1},a_{2},\ldots \right) \in K^{\mathbb {N}}\) be a sequence of elements of \(K\). Let \(a\in K\).

We say that the sequence \(\left( a_{i}\right) _{i\in \mathbb {N}}\) stabilizes to \(a\) if there exists some \(N\in \mathbb {N}\) such that

If \(a_{i}\) stabilizes to \(a\) as \(i\rightarrow \infty \), then we write \(\lim \limits _{i\rightarrow \infty }a_{i}=a\) and say that \(a\) is the limit (or eventual value) of \(\left( a_{i}\right) _{i\in \mathbb {N}}\). This is legitimate, since \(a\) is uniquely determined by the sequence \(\left( a_{i}\right) _{i\in \mathbb {N}}\).

The infinite product of a multipliable family \((f_n)_{n \in \mathbb {N}}\) is the FPS \(\prod _{n \in \mathbb {N}} f_n\) whose \(n\)-th coefficient equals \([x^n](\prod _{j=0}^{N} f_j)\) for any sufficiently large \(N\).

The infinite sum of a summable family \((f_n)_{n \in \mathbb {N}}\) is the FPS \(\sum _{n \in \mathbb {N}} f_n\) whose \(n\)-th coefficient is \(\sum _{i \in S_n} [x^n] f_i\), where \(S_n = \{ i : [x^n] f_i \neq 0\} \).

In this definition, we do not use Convention 1.210; thus, \(K\) can be an arbitrary commutative ring. However, we set \(K\left[\left[x\right]\right]_{1}=\left\{ f\in K\left[\left[x\right]\right]\ \mid \ \left[x^{0}\right]f=1\right\} \).

For any FPS \(f\in K\left[\left[x\right]\right]_{1}\), we define the logarithmic derivative \(\operatorname {loder}f\in K\left[\left[ x\right]\right]\) to be the FPS \(\frac{f^{\prime }}{f}\). (This is well-defined, since \(f\) is easily seen to be invertible.)

The logarithm series (or \(\overline{\log }\)) is the FPS

Its constant term is \(0\).

Let \(\left(\mathbf{a}_{i}\right)_{i\in I}\) be a (possibly infinite) family of FPSs. Then:

(a) The family \(\left(\mathbf{a}_{i}\right)_{i\in I}\) is said to be multipliable if and only if each coefficient in its product is finitely determined.

(b) If the family \(\left(\mathbf{a}_{i}\right)_{i\in I}\) is multipliable, then its product \(\prod _{i\in I}\mathbf{a}_{i}\) is defined to be the FPS whose \(x^{n}\)-coefficient (for any \(n\in \mathbb {N}\)) can be computed as follows: If \(n\in \mathbb {N}\), and if \(M\) is a finite subset of \(I\) that determines the \(x^{n}\)-coefficient in the product of \(\left( \mathbf{a}_{i}\right)_{i\in I}\), then

Let \(k\in \mathbb {N}\). The \(K\)-algebra of all FPSs in \(k\) variables \(x_{1},x_{2},\ldots ,x_{k}\) over \(K\) will be denoted by \(K\left[ \left[ x_{1},x_{2},\ldots ,x_{k}\right] \right] \).

Sometimes we will use different names for our variables. For example, if we work with \(2\) variables, we will commonly call them \(x\) and \(y\) instead of \(x_{1}\) and \(x_{2}\). Correspondingly, we will use the notation \(K\left[ \left[ x,y\right] \right] \) for the \(K\)-algebra of FPSs in these two variables.

The binomial generating function is the bivariate power series

whose coefficient at \(x^n y^k\) is \(\binom {n}{k}\).

The closed form of the binomial generating function is

Let \(f_0, f_1, f_2, \ldots \) be FPSs in a single variable \(x\). Define the bivariate power series \(\operatorname {embed}(f) := \sum _{k \in \mathbb {N}} f_k \, y^k \in K[[x,y]]\), whose coefficient at \(x^n y^k\) is the coefficient of \(x^n\) in \(f_k\).

Let \(\sigma \) be a type of variable indices and let \(i \in \sigma \). The partial derivative of a multivariate power series \(f = \sum _{\mathbf{m}} a_{\mathbf{m}}\, \mathbf{x}^{\mathbf{m}}\) with respect to \(x_i\) is the power series

where \(\mathbf{e}_i\) is the \(i\)-th standard basis vector (i.e., \(\mathbf{e}_i = (\delta _{j,i})_{j \in \sigma }\)).

This defines an \(R\)-linear map \(\partial /\partial x_i \colon R[[\mathbf{x}]] \to R[[\mathbf{x}]]\).

(a) The sum of two FPSs \(\mathbf{a}=\left( a_{0},a_{1},a_{2},\ldots \right)\) and \(\mathbf{b}=\left(b_{0},b_{1},b_{2},\ldots \right)\) is defined to be the FPS

It is denoted by \(\mathbf{a}+\mathbf{b}\).

(b) The difference of two FPSs \(\mathbf{a}=\left(a_{0},a_{1},a_{2},\ldots \right)\) and \(\mathbf{b}=\left(b_{0},b_{1},b_{2},\ldots \right)\) is defined to be the FPS

It is denoted by \(\mathbf{a}-\mathbf{b}\).

(c) If \(\lambda \in K\) and if \(\mathbf{a}=\left(a_{0},a_{1},a_{2},\ldots \right)\) is an FPS, then we define an FPS

(d) The product of two FPSs \(\mathbf{a}=\left(a_{0},a_{1},a_{2},\ldots \right)\) and \(\mathbf{b}=\left(b_{0},b_{1},b_{2},\ldots \right)\) is defined to be the FPS \(\left(c_{0},c_{1},c_{2},\ldots \right)\), where

This product is denoted by \(\mathbf{a}\cdot \mathbf{b}\) or just by \(\mathbf{ab}\).

(e) For each \(a\in K\), we define \(\underline{a}\) to be the FPS \(\left(a,0,0,0,\ldots \right)\). An FPS of the form \(\underline{a}\) for some \(a\in K\) (that is, an FPS \(\left(a_{0},a_{1},a_{2},\ldots \right)\) satisfying \(a_{1}=a_{2}=a_{3}=\cdots =0\)) is said to be constant.

(f) The set of all FPSs (in \(1\) indeterminate over \(K\)) is denoted \(K\left[\left[x\right]\right]\).

The partition generating function is

where \(p(n)\) denotes the number of partitions of \(n\).

(a) An FPS \(a\in K\left[ \left[ x\right] \right] \) is said to be a polynomial if all but finitely many \(n\in \mathbb {N}\) satisfy \(\left[ x^{n}\right] a=0\) (that is, if all but finitely many coefficients of \(a\) are \(0\)).

(b) We let \(K\left[ x\right] \) be the set of all polynomials \(a\in K\left[ \left[ x\right] \right] \). This set \(K\left[ x\right] \) is a subring of \(K\left[ \left[ x\right] \right] \) (according to Theorem 1.148 below), and is called the univariate polynomial ring over \(K\).

Let \(f\in K\left[\left[x\right]\right]\) be a polynomial FPS (in the sense of Definition 1.134). We define \(\operatorname {toPolynomial}(f)\in K[X]\) as the truncation of \(f\) at the degree bound given by Lemma 1.135.

Assume that \(K\) is a commutative \(\mathbb {Q}\)-algebra. Let \(f\in K\left[ \left[ x\right] \right] _{1}\) and \(c\in K\). Then, we define an FPS

(a) A sequence \(\left( k_{1},k_{2},k_{3},\ldots \right) \) is said to be essentially finite if all but finitely many \(i\in \left\{ 1,2,3,\ldots \right\} \) satisfy \(k_{i}=0\).

(b) A family \(\left( k_{i}\right) _{i\in I}\) is said to be essentially finite if all but finitely many \(i\in I\) satisfy \(k_{i}=0\).

Let \(f\) and \(g\) be two FPSs in \(K[[x]]\). Assume that \([x^0]g = 0\) (that is, \(g = g_1 x + g_2 x^2 + g_3 x^3 + \cdots \) for some \(g_1, g_2, g_3, \ldots \in K\)).

We then define an FPS \(f[g] \in K[[x]]\) as follows:

Write \(f\) in the form \(f = \sum _{n \in \mathbb {N}} f_n x^n\) with \(f_0, f_1, f_2, \ldots \in K\). (That is, \(f_n = [x^n]f\) for each \(n \in \mathbb {N}\).) Then, set

(This sum is well-defined, as we will see in Proposition 1.163 (b) below.)

This FPS \(f[g]\) is also denoted by \(f \circ g\), and is called the composition of \(f\) with \(g\), or the result of substituting \(g\) for \(x\) in \(f\).

Equivalently, the \(n\)-th coefficient of \(f[g]\) is the finite sum

A (possibly infinite) family \(\left(\mathbf{a}_{i}\right)_{i\in I}\) of FPSs is said to be summable (or entrywise essentially finite) if

In this case, the sum \(\sum _{i\in I}\mathbf{a}_{i}\) is defined to be the FPS with

A family \((f_i)_{i \in I}\) of FPSs in \(K[\! [x ]\! ]_0\) is summable if for each coefficient index \(n\), only finitely many \([x^n](f_i)\) are nonzero.

A family \((f_i)_{i \in I}\) of FPSs in \(K[\! [x ]\! ]_1\) is multipliable if for each coefficient index \(n\), all but finitely many \(f_i\) satisfy \([x^k](f_i - 1) = 0\) for all \(1 \le k \le n\).

For summable families, the coefficient-wise sum \(\sum _{i \in I} f_i\) belongs to \(K[\! [x ]\! ]_0\). For multipliable families, the product \(\prod _{i \in I} f_i\) belongs to \(K[\! [x ]\! ]_1\).

(a) An (integer) weak composition means a (finite) tuple of nonnegative integers.

(b) The size of a weak composition \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{m}\right) \) is defined to be the integer \(\alpha _{1}+\alpha _{2}+\cdots +\alpha _{m}\). It is written \(\left\vert \alpha \right\vert \).

(c) The length of a weak composition \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{m}\right) \) is defined to be the integer \(m\). It is written \(\ell \left( \alpha \right) \).

(d) Let \(n\in \mathbb {N}\). A weak composition of \(n\) means a weak composition whose size is \(n\).

(e) Let \(n\in \mathbb {N}\) and \(k\in \mathbb {N}\). A weak composition of \(n\) into \(k\) parts is a weak composition whose size is \(n\) and whose length is \(k\).

Let \(x\) denote the FPS \(\left(0,1,0,0,0,\ldots \right)\). In other words, let \(x\) denote the FPS with \(\left[x^{1}\right]x=1\) and \(\left[x^{i}\right]x=0\) for all \(i\neq 1\).

Let \(\left(\mathbf{a}_{i}\right)_{i\in I}\in K\left[\left[x\right]\right]^{I}\) be a (possibly infinite) family of FPSs. Let \(n\in \mathbb {N}\).

(a) We say that the \(x^{n}\)-coefficient in the sum of \(\left(\mathbf{a}_{i}\right)_{i\in I}\) is finitely determined if there is a finite subset \(M\) of \(I\) that determines the \(x^{n}\)-coefficient in the sum of \(\left(\mathbf{a}_{i}\right)_{i\in I}\).

(b) We say that the \(x^{n}\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i\in I}\) is finitely determined if there is a finite subset \(M\) of \(I\) that determines the \(x^{n}\)-coefficient in the product of \(\left(\mathbf{a}_{i}\right)_{i\in I}\).

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

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\).

Let \(A\) and \(B\) be two weighted sets. Then, the weighted set \(A+B\) is defined to be the disjoint union of \(A\) and \(B\), with the weight function inherited from \(A\) and \(B\) (meaning that each element of \(A\) has the same weight that it had in \(A\), and each element of \(B\) has the same weight that it had in \(B\)). Formally speaking, this means that \(A+B\) is the set \(\left( \left\{ 0\right\} \times A\right) \cup \left( \left\{ 1\right\} \times B\right) \), with the weight function given by

and

Let \(A\) and \(B\) be two weighted sets. Then, the weighted set \(A\times B\) is defined to be the Cartesian product of the sets \(A\) and \(B\) (that is, the set \(\left\{ \left( a,b\right) \ \mid \ a\in A\text{ and }b\in B\right\} \)), with the weight function defined as follows: For any \(\left( a,b\right) \in A\times B\), we set

(a) A weighted set is a set \(A\) equipped with a function \(w:A\rightarrow \mathbb {N}\), which is called the weight function of this weighted set. For each \(a\in A\), the value \(w\left( a\right) \) is denoted \(\left\vert a\right\vert \) and is called the weight of \(a\) (in our weighted set).

Usually, instead of explicitly specifying the weight function \(w\) as a function, we will simply specify the weight \(\left\vert a\right\vert \) for each \(a\in A\). The weighted set consisting of the set \(A\) and the weight function \(w\) will be called \(\left( A,w\right) \) or simply \(A\) when the weight function \(w\) is clear from the context.

(b) A weighted set \(A\) is said to be finite-type if for each \(n\in \mathbb {N}\), there are only finitely many \(a\in A\) having weight \(\left\vert a\right\vert =n\).

(c) If \(A\) is a finite-type weighted set, then the weight generating function of \(A\) is defined to be the FPS

This FPS is denoted by \(\overline{A}\).

(d) An isomorphism between two weighted sets \(A\) and \(B\) means a bijection \(\rho :A\rightarrow B\) that preserves the weight (i.e., each \(a\in A\) satisfies \(\left\vert \rho \left( a\right) \right\vert =\left\vert a\right\vert \)).

(e) We say that two weighted sets \(A\) and \(B\) are isomorphic (this is written \(A\cong B\)) if there exists an isomorphism between \(A\) and \(B\).

(a) For each even positive integer \(n\), we let \(A_{n}\) be the domino tiling of \(R_{n,3}\) consisting of the following dominos:

• the horizontal dominos \(\left\{ \left( 2i-1,\ 1\right) ,\ \left( 2i,\ 1\right) \right\} \) for all \(i\in \left[ n/2\right] \), which fill the bottom row of \(R_{n,3}\), and which we call the basement dominos;

• the vertical domino \(\left\{ \left( 1,2\right) ,\ \left( 1,3\right) \right\} \) in the first column, which we call the left wall;

• the vertical domino \(\left\{ \left( n,2\right) ,\ \left( n,3\right) \right\} \) in the last column, which we call the right wall;

• the horizontal dominos \(\left\{ \left( 2i,\ 2\right) ,\ \left( 2i+1,\ 2\right) \right\} \) for all \(i\in \left[ n/2-1\right] \), which fill the middle row of \(R_{n,3}\) (except for the first and last columns), and which we call the middle dominos;

• the horizontal dominos \(\left\{ \left( 2i,\ 3\right) ,\ \left( 2i+1,\ 3\right) \right\} \) for all \(i\in \left[ n/2-1\right] \), which fill the top row of \(R_{n,3}\) (except for the first and last columns), and which we call the top dominos.

(b) For each even positive integer \(n\), we let \(B_{n}\) be the domino tiling of \(R_{n,3}\) obtained by reflecting \(A_{n}\) across the horizontal axis of symmetry of \(R_{n,3}\) (swapping row \(1\) with row \(3\) and fixing row \(2\)).

(c) We let \(C\) denote the domino tiling of \(R_{2,3}\) consisting of three horizontal dominos: \(\left\{ (1,1),(2,1)\right\} \), \(\left\{ (1,2),(2,2)\right\} \), and \(\left\{ (1,3),(2,3)\right\} \).

(a) A family \(\left(a_{i}\right)_{i\in I}\in K^{I}\) of elements of \(K\) is said to be essentially finite if all but finitely many \(i\in I\) satisfy \(a_{i}=0\) (in other words, if the set \(\left\{ i\in I\ \mid \ a_{i}\neq 0\right\} \) is finite).

(b) Let \(\left(a_{i}\right)_{i\in I}\in K^{I}\) be an essentially finite family of elements of \(K\). Then, the infinite sum \(\sum _{i\in I}a_{i}\) is defined to equal the finite sum \(\sum _{\substack{[i, \in , I, ;, \\ , a, _, {, i, }, \neq , 0]}}a_{i}\). Such an infinite sum is said to be essentially finite.

A subset \(S \subseteq \{ 0, \ldots , n-1\} \) is \(d\)-blocky if \(S \subseteq \{ 0, \ldots , n-1\} \) and for each block index \(i \in \{ 0, \ldots , \lfloor n/d \rfloor - 1\} \), either all elements of \(\{ id, id+1, \ldots , id+d-1\} \) are in \(S\) or none are.

The evaluation map from \((\mathbb {Z}[z^{\pm }])[[q]]\) to \(\mathbb {Q}[[x]]\) is defined by sending a power series \(f = \sum _e c_e q^e\) (where \(c_e \in \mathbb {Z}[z^{\pm }]\)) to

where \(\widehat{c_e}(a,b,v,e)\) denotes the shifted evaluation that replaces each \(z^\ell \) in \(c_e\) by \(v^\ell x^{ae+b\ell }\).

For any partition \(\lambda =(\lambda _{1},\lambda _{2},\ldots ,\lambda _{k})\) and any \(\ell \in \mathbb {Z}\), the excited state \(E_{\ell ,\lambda }\) is defined by starting with the \(\ell \)-ground state \(G_{\ell }\) and then successively letting the \(k\) electrons at the highest levels jump \(\lambda _{1},\lambda _{2},\ldots ,\lambda _{k}\) steps to the right, respectively:

Given a pair \((P, N)\) of finite subsets of \(\mathbb {N}\), define the state \(\operatorname {fromFinsetPair}(P, N)\) whose levels are

Here \(P\) encodes the nonneg levels present, and \(N\) encodes the negative levels missing (with \(n \in N\) meaning level \(-(n+1)\) is missing).

For \(\ell \in \mathbb {Z}\), the \(\ell \)-ground state is

The \(q\)-only product is

The \(z\)-dependent product is

If \(S\) is a state, \(p\in S\), and \(q\) is a positive integer such that \(p+q\notin S\), then the state

is said to be obtained from \(S\) by letting the electron at level \(p\) jump \(q\) steps to the right.

The partition generating function in JacobiRing is

The sum-of-divisors generating function is

where \(\sigma (k) = \sigma _1(k) = \sum _{d\mid k} d\) is the sum of positive divisors of \(k\).

A level is a number of the form \(p+\frac{1}{2}\) with \(p\in \mathbb {Z}\). A state is a set of levels that contains all but finitely many negative levels, and only finitely many positive levels.

For any state \(S\), we define:

• the energy of \(S\) to be

  \[ \operatorname {energy}S:=\sum _{\substack{[p, {\gt}, 0, ;, \\ , p, \in , S]}}2p -\sum _{\substack{[p, {\lt}, 0, ;, \\ , p, \notin , S]}}2p \in \mathbb {N}; \]

• the particle number of \(S\) to be

  \[ \operatorname {parnum}S:=\left(\text{\# of positive levels in } S\right) -\left(\text{\# of negative levels not in } S\right)\in \mathbb {Z}. \]

The state generating function is the formal sum over all integer–partition pairs \((\ell , \mu )\):

It is defined as the formal sum \(\sum '_{(\ell , \mu )} q^{\ell ^2 + 2|\mu |} z^\ell \) over all integer–partition pairs.

The state monomial with energy \(e\) and particle number \(p\) is the element \(q^e z^p \in (\mathbb {Z}[z^{\pm }])[[q]]\).

If \(i\) and \(j\) are any objects, then \(\delta _{i,j}\) means the element

of \(K\).

The set \(\binom {[n]}{k}\) of \(k\)-element subsets of \(\{ 0, \ldots , n-1\} \):

Let \(\mathbf{p} = (p_1, \ldots , p_k)\) be a path tuple.

(a) A vertex \(v\) is crowded in \(\mathbf{p}\) if \(v\) lies on at least two distinct paths \(p_i, p_j\) with \(i \ne j\).

(b) The crowded path indices of \(\mathbf{p}\) is the set of indices \(i\) such that \(p_i\) contains a vertex shared with some other path \(p_j\).

(c) For an ipat \(\mathbf{p}\), the minimum crowded path index is the smallest \(i\) in the crowded path indices.

(d) The crowded vertices on path \(i\) is the set of vertices on \(p_i\) that also appear on some other path.

We consider the infinite simple digraph with vertex set \(\mathbb {Z}^{2}\) (so the vertices are pairs of integers) and arcs

and

The arcs of the first form are called east-steps or right-steps; the arcs of the second form are called north-steps or up-steps.

The vertices of this digraph will be called lattice points or grid points or simply points.

The entire digraph will be denoted by \(\mathbb {Z}^{2}\) and called the integer lattice or integer grid.

Any path is uniquely determined by its starting point and its step sequence.

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

(a) A \(k\)-vertex means a \(k\)-tuple of lattice points.

(b) If \(\mathbf{A}=\left( A_{1},A_{2},\ldots ,A_{k}\right) \) is a \(k\)-vertex, and if \(\sigma \in S_{k}\) is a permutation, then \(\sigma \left( \mathbf{A}\right) \) shall denote the \(k\)-vertex \(\left( A_{\sigma \left( 1\right) },A_{\sigma \left( 2\right) },\ldots ,A_{\sigma \left( k\right) }\right) \).

(c) If \(\mathbf{A}=\left( A_{1},A_{2},\ldots ,A_{k}\right) \) and \(\mathbf{B}=\left( B_{1},B_{2},\ldots ,B_{k}\right) \) are two \(k\)-vertices, then a path tuple from \(\mathbf{A}\) to \(\mathbf{B}\) means a \(k\)-tuple \(\left( p_{1},p_{2},\ldots ,p_{k}\right) \), where each \(p_{i}\) is a path from \(A_{i}\) to \(B_{i}\).

(d) A path tuple \(\left( p_{1},p_{2},\ldots ,p_{k}\right) \) is said to be non-intersecting if no two of the paths \(p_{1},p_{2},\ldots ,p_{k}\) have any vertex in common. We abbreviate “non-intersecting path tuple” as nipat.

(e) A path tuple \(\left( p_{1},p_{2},\ldots ,p_{k}\right) \) is said to be intersecting if it is not non-intersecting (i.e., if two of its paths have a vertex in common). We abbreviate “intersecting path tuple” as ipat.

Let \(k \in \mathbb {N}\) and let \(\mathbf{A}, \mathbf{B}\) be two \(k\)-vertices.

(a) The path count matrix \(M\) is the \(k \times k\) integer matrix with entries \(M_{i,j} = \# \mathrm{paths}(A_i \to B_j)\).

(b) For \(\sigma \in S_k\), the number of nipats from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\).

(c) For \(\sigma \in S_k\), the number of ipats from \(\mathbf{A}\) to \(\sigma (\mathbf{B})\).

Given four lattice points \(A, A', B, B'\):

(a) A signed path tuple is a pair of paths \((p_0, p_1)\) together with a sign flag indicating whether the destinations are \((B, B')\) (sign \(+1\)) or \((B', B)\) (sign \(-1\)).

(b) The path count matrix is the \(2 \times 2\) integer matrix with entries \(\# \mathrm{paths}(A_i \to B_j)\).

(c) The number of nipats from \((A, A')\) to \((B, B')\).

Let \(a\) be a real number.

Then, \(\left\lfloor a\right\rfloor \) (called the floor of \(a\)) means the largest integer that is \(\leq a\).

Likewise, \(\left\lceil a\right\rceil \) (called the ceiling of \(a\)) means the smallest integer that is \(\geq a\).

The partition generating function \(P := \sum _{n\ge 0} p(n) x^n \in \mathbb {Z}[[x]]\) and the divisor sum generating function \(S := \sum _{k\ge 1} \sigma (k) x^k \in \mathbb {Z}[[x]]\).

We will use the Iverson bracket notation: If \(\mathcal{A}\) is a logical statement, then \(\left[ \mathcal{A} \right]\) means the truth value of \(\mathcal{A}\); this is the integer \(\begin{cases} 1, & \text{if }\mathcal{A}\text{ is true};\\ 0, & \text{if }\mathcal{A}\text{ is false}. \end{cases} \)

Note that the Kronecker delta notation is a particular case of the Iverson bracket: We have

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

(a) A partition of \(n\) into odd parts means a partition of \(n\) whose all parts are odd.

(b) A partition of \(n\) into distinct parts means a partition of \(n\) whose parts are distinct.

(c) Let

(a) An (integer) partition means a (finite) weakly decreasing tuple of positive integers – i.e., a finite tuple \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{m}\right) \) of positive integers such that \(\lambda _{1}\geq \lambda _{2}\geq \cdots \geq \lambda _{m}\).

Thus, partitions are the same as weakly decreasing compositions. Hence, the notions of size and length of a partition are automatically defined, since we have defined them for compositions (in Definition 1.291).

(b) The parts of a partition \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{m}\right) \) are simply its entries \(\lambda _{1},\lambda _{2},\ldots ,\lambda _{m}\).

(c) Let \(n\in \mathbb {Z}\). A partition of \(n\) means a partition whose size is \(n\).

(d) Let \(n\in \mathbb {Z}\) and \(k\in \mathbb {N}\). A partition of \(n\) into \(k\) parts is a partition whose size is \(n\) and whose length is \(k\).

Let \(k,\ell \in \mathbb {N}\).

1. \(q_{k,\ell }(n) := |\{ p \vdash n : \ell (p) = k,\; \text{largest part of }p = \ell \} |\).

2. \(Q(k,\ell ) := \sum _{n=k}^{k\ell } q_{k,\ell }(n)\), the total number of such partitions over all valid sizes.

For any \(k\in \mathbb {Z}\), define a nonnegative integer \(w_{k}\in \mathbb {N}\) by

This is called the \(k\)-th pentagonal number.

(a) Let \(n\in \mathbb {Z}\) and \(k\in \mathbb {N}\). Then, we set

(b) Let \(n\in \mathbb {Z}\). Then, we set

This is called the \(n\)-th partition number.

Let \(n\in \mathbb {N}\) and \(k\in \mathbb {Z}\).

(a) The \(q\)-binomial coefficient (or Gaussian binomial coefficient) \(\binom {n}{k}_{q}\) is defined to be the polynomial

(b) If \(a\) is any element of a ring \(A\), then we set

(a) For any \(n\in \mathbb {N}\), define the \(q\)-integer \([n]_{q}\) to be

(b) For any \(n\in \mathbb {N}\), define the \(q\)-factorial \([n]_{q}!\) to be

(c) As usual, if \(a\) is an element of a ring \(A\), then \([n]_{a}\) and \([n]_{a}!\) will mean the results of substituting \(a\) for \(q\) in \([n]_{q}\) and \([n]_{q}!\), respectively. Thus, explicitly, \([n]_{a}=a^{0}+a^{1}+\cdots +a^{n-1}\) and \([n]_{a}!=[1]_{a}[2]_{a}\cdots [n]_{a}\).

Given a partition of \(n\) that contains \(1\) as a part, removing one copy of \(1\) yields a partition of \(n-1\). Conversely, adding one copy of \(1\) to a partition of \(n\) yields a partition of \(n+1\).

Given a partition of \(n\) into \(k\) parts with all parts \({\gt}1\), subtracting \(1\) from each part yields a partition of \(n-k\) into \(k\) parts. Conversely, adding \(1\) to each part of a partition of \(n\) into \(k\) parts produces a partition of \(n+k\) into \(k\) parts.

The partner of a finite set \(I\) of natural numbers is the symmetric difference \(I' := I \bigtriangleup \{ 0\} \). If \(0 \in I\), then \(I' = I \setminus \{ 0\} \); if \(0 \notin I\), then \(I' = I \cup \{ 0\} \).

Define the \(n\times n\) Pascal matrix, the lower triangular factor \(L\), and the upper triangular factor \(U\) by:

for \(0\le i,j,k \le n-1\).

The pentagonal coefficient at \(n\in \mathbb {N}\) is

This is well-defined by the injectivity of pentagonal numbers (Lemma 2.69).

The Euler product is the infinite product

defined as a multipliable product in the Pi topology on \(R[[x]]\).

The pentagonal series is the formal power series

The canonical reduced word for \(\sigma \) is the concatenation of Lehmer blocks:

Let \(X\) be a set. Let \(i_1, i_2, \ldots , i_k\) be \(k\) distinct elements of \(X\). Then,

means the permutation of \(X\) that sends

and leaves all other elements of \(X\) unchanged. In other words, \(\operatorname {cyc}_{i_1, i_2, \ldots , i_k}\) means the permutation of \(X\) that satisfies

for every \(p \in X\), where \(i_{k+1}\) means \(i_1\).

This permutation is called a \(k\)-cycle.

Let \(X\) be a finite set. Let \(\sigma \) be a permutation of \(X\).

(a) The cycles of \(\sigma \) are defined to be the cycles in the DCD of \(\sigma \) (as defined in Theorem 3.123 (a)). (This includes \(1\)-cycles, if there are any in the DCD of \(\sigma \).)

We shall equate a cycle of \(\sigma \) with any of its cyclic rotations; thus, for example, \(\left( 3,1,4\right) \) and \(\left( 1,4,3\right) \) shall be regarded as being the same cycle (but \(\left( 3,1,4\right) \) and \(\left( 3,4,1\right) \) shall not).

(b) The cycle lengths partition of \(\sigma \) shall denote the partition of \(\left\vert X\right\vert \) obtained by writing down the lengths of the cycles of \(\sigma \) in weakly decreasing order.

Let \(n \in \mathbb {N}\). A permutation \(\sigma \in S_n\) is said to be

• even if \((-1)^{\sigma } = 1\) (that is, if \(\ell (\sigma )\) is even);

• odd if \((-1)^{\sigma } = -1\) (that is, if \(\ell (\sigma )\) is odd).

A cell \((i, j)\) is in the Rothe diagram of \(\sigma \) if \(j {\lt} \sigma (i)\) and \(i {\lt} \sigma ^{-1}(j)\). These are the cells that are not “hit” by either the row or column of a permutation matrix entry.

The explicit bijection between inversions of \(\sigma \) and inversions of \(\sigma ^{-1}\), sending \((i,j)\) to \((\sigma (j), \sigma (i))\).

Let \(X\) be a set. An involution of \(X\) means a map \(f : X \to X\) that satisfies \(f \circ f = \operatorname {id}\). Clearly, an involution is always a permutation, and equals its own inverse.

Let \(n\in \mathbb {N}\) and \(\sigma \in S_{n}\).

(a) An inversion of \(\sigma \) means a pair \(\left(i,j\right)\) of elements of \(\left[n\right]\) such that \(i{\lt}j\) and \(\sigma \left(i\right) {\gt}\sigma \left(j\right)\).

(b) The length (also known as the Coxeter length) of \(\sigma \) is the # of inversions of \(\sigma \). It is called \(\ell \left( \sigma \right)\).

A word \(w = (k_1, \ldots , k_q)\) is reduced if its length \(q\) equals \(\ell (s_{k_1} \cdots s_{k_q})\).

For \(\sigma \in S_n\) and \(i \in [n]\), define \(g(\sigma , i) = |\{ j {\lt} i : \sigma (j) {\gt} \sigma (i)\} |\). This counts inversions with \(i\) as the second element.

Let \(\left(a_{1},a_{2},\ldots ,a_{n}\right)\) and \(\left(b_{1},b_{2},\ldots ,b_{n}\right)\) be two \(n\)-tuples of integers. We say that

if and only if

• there exists some \(k\in \left[n\right]\) such that \(a_{k}\neq b_{k}\), and

• the smallest such \(k\) satisfies \(a_{k}{\lt}b_{k}\).

The relation \({\lt}_{\operatorname {lex}}\) is a strict total order on \(\mathbb {Z}^n\) (the lexicographic order).

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

(a) For each \(\sigma \in S_{n}\) and \(i\in \left[n\right]\), we set

(b) For each \(m\in \mathbb {Z}\), we let \(\left[m\right]_{0}\) denote the set \(\left\{ 0,1,\ldots ,m\right\} \). (This is an empty set when \(m{\lt}0\).)

(c) We let \(H_{n}\) denote the set

This set \(H_{n}\) has size \(n!\).

(d) Each \(\sigma \in S_n\) and each \(i\in [n]\) satisfy \(\ell _i(\sigma ) \in \{ 0,1,\ldots ,n-i\} = [n-i]_0\).

(e) We define the map

If \(\sigma \in S_{n}\) is a permutation, then the \(n\)-tuple \(L\left(\sigma \right)\) is called the Lehmer code (or just the code) of \(\sigma \).

For each \(i \in [n]\), we define the Lehmer block \(a_i\) as

where \(i' = i + \ell _i(\sigma )\) and \(\ell _i(\sigma )\) is the Lehmer entry at position \(i\). If \(\ell _i(\sigma ) = 0\), then \(a_i = \mathrm{id}\) (the empty product). The product \(a_i\) equals the cycle \((i', i'-1, \ldots , i)\).

The non-inversions of a permutation \(\sigma \in S_n\) are the pairs \((i,j)\) with \(i {\lt} j\) and \(\sigma (i) {\lt} \sigma (j)\). These are exactly the ordered pairs that are not inversions. The inversions and non-inversions partition the set of all \(\binom {n}{2}\) ordered pairs.

Let \(n \in \mathbb {N}\) and \(\sigma \in S_n\). We introduce three notations for \(\sigma \):

(a) A two-line notation of \(\sigma \) means a \(2 \times n\)-array

where the entries \(p_1, p_2, \ldots , p_n\) of the top row are the \(n\) elements of \([n]\) in some order. Commonly, we pick \(p_i = i\).

(b) The one-line notation (short, OLN) of \(\sigma \) means the \(n\)-tuple \((\sigma (1), \sigma (2), \ldots , \sigma (n))\).

(c) The cycle digraph of \(\sigma \) is the directed graph with vertices \(1, 2, \ldots , n\) and arcs \(i \to \sigma (i)\) for all \(i \in [n]\).

Let \(X\) be a set.

(a) A permutation of \(X\) means a bijection from \(X\) to \(X\).

(b) It is known that the set of all permutations of \(X\) is a group under composition. This group is called the symmetric group of \(X\), and is denoted by \(S_X\). Its neutral element is the identity map \(\operatorname {id}_X : X \to X\). Its size is \(|X|!\) when \(X\) is finite.

(c) As usual in group theory, we will write \(\alpha \beta \) for the composition \(\alpha \circ \beta \) when \(\alpha , \beta \in S_X\). This is the map that sends each \(x \in X\) to \(\alpha (\beta (x))\).

(d) If \(\alpha \in S_X\) and \(i \in \mathbb {Z}\), then \(\alpha ^i\) shall denote the \(i\)-th power of \(\alpha \) in the group \(S_X\). Note that \(\alpha ^i = \underbrace{\alpha \circ \alpha \circ \cdots \circ \alpha }_{i\text{ times}}\) if \(i \ge 0\). Also, \(\alpha ^0 = \operatorname {id}_X\). Also, \(\alpha ^{-1}\) is the inverse of \(\alpha \) in the group \(S_X\), that is, the inverse of the map \(\alpha \).

The set \(A\) from the transposition length proof: \(A = \{ a {\lt} i \mid \sigma (j) {\lt} \sigma (a) {\lt} \sigma (i)\} \). These elements produce paired lost and gained inversions: \((a, j)\) is lost and \((a, i)\) is gained.

The set \(B\) from the transposition length proof: \(B = \{ b {\gt} j \mid \sigma (j) {\lt} \sigma (b) {\lt} \sigma (i)\} \). These elements produce paired lost and gained inversions: \((i, b)\) is lost and \((j, b)\) is gained.

The set \(Q\) from Proposition 3.59: \(Q = \{ k \in \{ i+1, \ldots , j-1\} \mid \sigma (j) {\lt} \sigma (k) {\lt} \sigma (i)\} \).

The set \(R\) from Proposition 3.59: \(R = \{ k \in \{ i+1, \ldots , j-1\} \mid \sigma (i) {\lt} \sigma (k) {\lt} \sigma (j)\} \).

Let \(n \in \mathbb {N}\) and \(i \in [n-1]\). Then, the simple transposition \(s_i\) is defined by

Let \(n \in \mathbb {N}\). The sign of a permutation \(\sigma \in S_n\) is defined to be the integer \((-1)^{\ell (\sigma )}\).

It is denoted by \((-1)^{\sigma }\) or \(\operatorname {sgn}(\sigma )\) or \(\operatorname {sign}(\sigma )\) or \(\varepsilon (\sigma )\). It is also known as the signature of \(\sigma \).

For \(\sigma \in S_n\) and \(i \in [n]\), define \(s(\sigma , i) = |\{ j {\lt} i : \sigma (j) {\lt} \sigma (i)\} |\). This counts positions before \(i\) with smaller values.

Let \(n \in \mathbb {Z}\). Then, \([n]\) shall mean the set \(\{ 1, 2, \ldots , n\} \). This is an \(n\)-element set if \(n \ge 0\), and is an empty set if \(n \le 0\).

The symmetric group \(S_{[n]}\) (consisting of all permutations of \([n]\)) will be denoted \(S_n\) and called the \(n\)-th symmetric group. Its size is \(n!\) (when \(n \ge 0\)).

Let \(i\) and \(j\) be two distinct elements of a set \(X\).

Then, the transposition \(t_{i,j}\) is the permutation of \(X\) that sends \(i\) to \(j\), sends \(j\) to \(i\), and leaves all other elements of \(X\) unchanged.

A word (of length \(q\)) in \(S_n\) is a finite sequence \((k_1, k_2, \ldots , k_q)\) where each \(k_i \in \{ 0, 1, \ldots , n-2\} \) is an index of a simple transposition.

The product of a word \(w = (k_1, \ldots , k_q)\) is the permutation \(s_{k_1} s_{k_2} \cdots s_{k_q}\).

A derangement of a set \(X\) means a permutation of \(X\) that has no fixed points.

The number of surjective maps from \([m]\) to \([n]\) is defined as

Let \(f\in K\left[ x\right] \) be a polynomial. Let \(A\) be any \(K\)-algebra. Let \(a\in A\) be any element. We then define an element \(f\left[ a\right] \in A\) as follows:

Write \(f\) in the form \(f=\sum _{n\in \mathbb {N}}f_{n}x^{n}\) with \(f_{0},f_{1},f_{2},\ldots \in K\). (That is, \(f_{n}=\left[ x^{n}\right] f\) for each \(n\in \mathbb {N}\).) Then, set

(This sum is essentially finite, since \(f\) is a polynomial.)

The element \(f\left[ a\right] \) is also denoted by \(f\circ a\) or by \(f\left( a\right) \), and is called the value of \(f\) at \(a\) (or the evaluation of \(f\) at \(a\), or the result of substituting \(a\) for \(x\) in \(f\)).

The \(q\)-binomial coefficient \(\binom {n}{k}_q\) is the polynomial in \(\mathbb {Z}[q]\) defined by

where \(\operatorname {sum}(S) = \sum _{x \in S} x\). This is the local definition used in the formalization; it agrees with Mathlib’s \(q\)-binomial coefficient (see Lemma 4.19).

The \(q\)-binomial coefficient as a polynomial in \(\mathbb {Z}[q]\) via the partition sum:

where \(c(s,k,m)\) is the number of partitions of \(s\) fitting in a \(k \times m\) box. The evaluation \(\binom {n}{k}_a\) is obtained by substituting \(a\) for \(q\).

The span map sends a linearly independent \(k\)-tuple \((v_1, \ldots , v_k)\) in \(V\) to its span \(\mathrm{span}(v_1, \ldots , v_k)\), viewed as a \(k\)-dimensional subspace.

The sequence \((a_n)\) defined by \(a_0 = 1\) and \(a_{n+1} = 2a_n + n\) for all \(n\geq 0\).

Let \(K\) be a field. Let \(d\) be a positive integer.

(a) A \(d\)-th root of unity in \(K\) means an element \(\omega \) of \(K\) satisfying \(\omega ^d = 1\).

(b) A primitive \(d\)-th root of unity in \(K\) means an element \(\omega \) of \(K\) satisfying \(\omega ^d = 1\) but \(\omega ^i \neq 1\) for each \(i \in \{ 1, 2, \ldots , d-1\} \). In other words, a primitive \(d\)-th root of unity in \(K\) means an element of the multiplicative group \(K^{\times }\) whose order is \(d\).

The sign of a finite set \(I\) of natural numbers is \(\operatorname {sign}(I) := (-1)^{|I|}\).

A skew tableau \(T\) of shape \(\lambda /\mu \) has all entries zero if every cell \((i, j) \in Y(\lambda /\mu )\) satisfies \(T(i, j) = 0\). This is the key property characterizing Yamanouchi tableaux for the row partition \(\nu = (n, 0, \ldots , 0)\).

(a) We let \(\rho \) be the \(N\)-tuple \(\left( N-1,N-2,\ldots ,N-N\right) \in \mathbb {N}^{N}\).

(b) For any \(N\)-tuple \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{N}\right) \in \mathbb {N}^{N}\), we define

This is called the \(\alpha \)-alternant (of \(x_{1},x_{2},\ldots ,x_{N}\)).

A polynomial \(f \in \mathcal{P}\) is antisymmetric if

Let \(T\) be a semistandard tableau and let \(k {\lt} N-1\). A cell \(c = (i,j)\) with \(T(c) = k\) is forced if there exists a cell \((i+1,j)\) directly below with \(T(i+1,j) = k+1\). Similarly for \(T(c) = k+1\) with a cell directly above having value \(k\). Free cells are those that are not forced.

Among the free cells, the parenthesis-matching algorithm classifies each as matched or unmatched: reading free entries left-to-right in each row, each free \((k{+}1)\) matches with the nearest unmatched free \(k\) to its left. Unmatched entries are those remaining after this process.

The Bender–Knuth involution \(\mathrm{BK}_k\) on fillings of \(Y(\lambda /\mu )\). For a semistandard filling \(f\), \(\mathrm{BK}_k(f)\) swaps certain entries \(k\) and \(k{+}1\) while preserving semistandardness. For non-semistandard fillings, it returns the input unchanged.

Let \(T\) be a semistandard tableau of shape \(\lambda /\mu \) and let \(k {\lt} N-1\). The Bender–Knuth involution \(\beta _k(T)\) is obtained from \(T\) by swapping only the unmatched free \(k\)’s and unmatched free \((k{+}1)\)’s:

Forced cells and matched free cells are left unchanged.

The prefix-restricted BK involution \(\beta _k^{{\lt}j}\) applies the parenthesis-matching swap of \(k\) and \(k{+}1\) only to cells in columns \({\lt} j\). Cells in columns \(\geq j\) are left unchanged:

The column partition \((1, 1, \ldots , 1, 0, \ldots , 0)\) with \(n\) ones (i.e., \(n\) boxes in the first column). This is the partition corresponding to \(e_n\). Requires \(n \leq N\).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. Let \(T\) be a tableau of shape \(\lambda /\mu \). Let \(j\) be a positive integer. Then, \(\operatorname {col}_{\geq j}T\) means the restriction of \(T\) to columns \(j,j+1,j+2,\ldots \) (that is, the result of removing the first \(j-1\) columns from \(T\)). Formally speaking, this means the restriction of the map \(T\) to the set \(\left\{ \left( u,v\right) \in Y\left( \lambda /\mu \right) \ \mid \ v\geq j\right\} \).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. Let \(T\) be a tableau of shape \(\lambda /\mu \). We define the content of \(T\) to be the \(N\)-tuple \(\left( a_{1},a_{2},\ldots ,a_{N}\right) \), where

We denote this \(N\)-tuple by \(\operatorname *{cont}T\).

(a) For each \(n \in \mathbb {Z}\), define a symmetric polynomial \(e_n \in \mathcal{S}\) by

This \(e_n\) is called the \(n\)-th elementary symmetric polynomial in \(x_1, x_2, \ldots , x_N\).

(b) For each \(n \in \mathbb {Z}\), define a symmetric polynomial \(h_n \in \mathcal{S}\) by

This \(h_n\) is called the \(n\)-th complete homogeneous symmetric polynomial in \(x_1, x_2, \ldots , x_N\).

(c) For each \(n \in \mathbb {Z}\), define a symmetric polynomial \(p_n \in \mathcal{S}\) by

This \(p_n\) is called the \(n\)-th power sum in \(x_1, x_2, \ldots , x_N\).

The \(N\)-partition \((1, 1, \ldots , 1, 0, 0, \ldots , 0)\) with \(n\) ones and \(N - n\) zeros.

The \(N\)-partition \((n, 0, 0, \ldots , 0)\) with \(n\) in the first position and zeros elsewhere.

A filling of a skew Young diagram \(Y(\lambda /\mu )\) is a function \(f : Y(\lambda /\mu ) \to [N]\). A filling is semistandard if it satisfies the row-weak and column-strict conditions. The filling monomial is \(x_f = \prod _{c \in Y(\lambda /\mu )} x_{f(c)}\).

The content of a filling \(f\) of \(Y(\lambda /\mu )\) is the function \(\mathrm{cont}(f) : [N] \to \mathbb {N}\) defined by

Convert a subset \(s \subseteq \mathrm{Fin}\, N\) of size \(n\) to an SSYT of column partition shape \((1^n, 0^{N-n})\): column \(0\) contains the sorted elements of \(s\) in strictly increasing order.

The finite set of \(N\)-partitions \(\lambda \) such that \(\lambda /\mu \) is a horizontal \(n\)-strip. This is computed by filtering all functions bounded by the horizontal strip constraints for weak decrease, horizontal strip condition, and size difference.

The \(R\)-algebra homomorphism from \(R[x_1, \ldots , x_n]\) to the symmetric subalgebra sending \(x_i\) to \(h_{i+1}\). This is the analogous construction to the elementary symmetric algebra homomorphism (which sends \(x_i\) to \(e_{i+1}\)), using complete homogeneous instead of elementary symmetric polynomials.

The extended \(h_n\): \(h_n = 0\) for \(n {\lt} 0\), \(h_0 = 1\). This is needed since the Jacobi–Trudi formula may have negative indices.

Two functions \(\lambda : \mathrm{Fin}\, N \to \mathbb {N}\) and \(\lambda ^t : \mathrm{Fin}\, M \to \mathbb {N}\) are transposes of each other if for all \(i {\lt} N\) and \(j {\lt} M\):

This is the symmetric characterization of the transpose relation between Young diagrams.

The arc weight function for the Jacobi–Trudi proof on the integer lattice \(\mathbb {Z}^2\): east-steps at height \(y\) (with \(1 \leq y \leq N\)) are weighted by \(x_{y-1}\); north-steps are weighted by \(1\).

Define two \(N\)-vertices \(\mathbf{A} = (A_1, \ldots , A_N)\) and \(\mathbf{B} = (B_1, \ldots , B_N)\) by

Convert an LGV path (in the integer lattice digraph) from \((a, 1)\) to \((c, N)\) into a lattice path by extracting the \(y\)-coordinates at which east-steps occur and converting them to \(\mathrm{Fin}\, N\) values (by subtracting \(1\)).

Let \(\lambda \) be any \(N\)-partition. Then, we define a symmetric polynomial \(m_{\lambda }\in \mathcal{S}\) by

This is called the monomial symmetric polynomial corresponding to \(\lambda \).

(a) A monomial is an expression of the form \(x_1^{a_1} x_2^{a_2} \cdots x_N^{a_N}\) with \(a_1, a_2, \ldots , a_N \in \mathbb {N}\).

(b) The degree \(\deg \mathfrak {m}\) of a monomial \(\mathfrak {m} = x_1^{a_1} x_2^{a_2} \cdots x_N^{a_N}\) is defined to be \(a_1 + a_2 + \cdots + a_N \in \mathbb {N}\).

(c) A monomial \(\mathfrak {m} = x_1^{a_1} x_2^{a_2} \cdots x_N^{a_N}\) is said to be squarefree if \(a_1, a_2, \ldots , a_N \in \{ 0,1\} \). (This is saying that no square or higher power of an indeterminate appears in \(\mathfrak {m}\); thus the name “squarefree”.)

(d) A monomial \(\mathfrak {m} = x_1^{a_1} x_2^{a_2} \cdots x_N^{a_N}\) is said to be primal if there is at most one \(i \in [N]\) satisfying \(a_i {\gt} 0\). (This is saying that the monomial \(\mathfrak {m}\) contains no two distinct indeterminates. Thus, a primal monomial is just \(1\) or a power of an indeterminate.)

A non-intersecting path tuple (nipat) from \(\mathbf{A} = (A_1, \ldots , A_N)\) to \(\mathbf{B} = (B_1, \ldots , B_N)\) is an \(N\)-tuple of lattice paths \((p_1, \ldots , p_N)\) where \(p_i\) goes from \((\mu _i - i, 1)\) to \((\lambda _i - i, N)\), subject to a column-strictness condition: for \(i {\lt} j\), if east steps \(k\) (in path \(i\)) and \(k'\) (in path \(j\)) correspond to the same tableau column (\(\mu _i + k = \mu _j + k'\)), then the height of path \(i\) at step \(k\) is strictly less than the height of path \(j\) at step \(k'\).

The weight of a nipat is \(\prod _{i} w(p_i)\).

The forward map of the nipat–SSYT bijection: given a nipat \(\mathbf{p} = (p_1, \ldots , p_N)\), construct the skew SSYT \(T(\mathbf{p})\) of shape \(\lambda /\mu \) whose \(i\)-th row contains the east-step heights of path \(p_i\).

Row-weakness follows from the weakly increasing property of each path’s east-step heights. Column-strictness follows from the column-strictness condition of the nipat.

An \(N\)-partition will mean a weakly decreasing \(N\)-tuple of nonnegative integers. In other words, an \(N\)-partition means an \(N\)-tuple \(\left( \lambda _{1},\lambda _{2},\ldots ,\lambda _{N}\right) \in \mathbb {N}^{N}\) with \(\lambda _{1}\geq \lambda _{2}\geq \cdots \geq \lambda _{N}\).

The size (or weight) of an \(N\)-partition \(\lambda = (\lambda _1, \lambda _2, \ldots , \lambda _N)\) is defined to be \(|\lambda | := \lambda _1 + \lambda _2 + \cdots + \lambda _N\).

We define a partial order on \(N\)-partitions by componentwise comparison: \(\mu \leq \nu \) iff \(\mu _i \leq \nu _i\) for all \(i \in [N]\).

The skew Young diagram \(Y(\lambda /\mu )\) for \(N\)-partitions \(\lambda , \mu \) is the set difference \(Y(\lambda ) \setminus Y(\mu )\), consisting of cells \((i, j)\) with \(\mu _i \leq j {\lt} \lambda _i\).

The Young diagram \(Y(\lambda )\) of an \(N\)-partition \(\lambda \) is the finite set of cells

The transpose (or conjugate) of an \(N\)-partition \(\lambda \) is the partition \(\lambda ^t\) whose \(i\)-th part equals \(|\{ j : j {\lt} N,\; \lambda _j {\gt} i\} |\), i.e., the number of parts of \(\lambda \) that exceed \(i\). Requires \(N {\gt} 0\); the result is a partition of length \(\lambda _1\).

The finite set of \(N\)-partitions of size \(n\).

The \(\omega \)-involution promoted to an algebra equivalence \(\omega : \Lambda _R \xrightarrow {\sim } \Lambda _R\).

The \(\omega \)-involution on the symmetric subalgebra, defined as the composition of the complete homogeneous algebra homomorphism with the inverse of the elementary symmetric algebra equivalence. This maps \(e_k \mapsto h_k\) for \(1 \leq k \leq n\) and extends algebraically to all symmetric polynomials.

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions.

We say that \(\mu \subseteq \lambda \) if and only if \(Y\left( \mu \right) \subseteq Y\left( \lambda \right) \). Equivalently, \(\mu \subseteq \lambda \) if and only if

Thus we have defined a partial order \(\subseteq \) on the set of all \(N\)-partitions.

(a) Let \(\mathcal{P}\) be the polynomial ring \(K[x_1, x_2, \ldots , x_N]\) in \(N\) variables over \(K\). This is not just a ring; it is a commutative \(K\)-algebra.

(b) The symmetric group \(S_N\) acts on the set \(\mathcal{P}\) according to the formula

Here, \(f[a_1, a_2, \ldots , a_N]\) means the result of substituting \(a_1, a_2, \ldots , a_N\) for the indeterminates \(x_1, x_2, \ldots , x_N\) in a polynomial \(f \in \mathcal{P}\).

Roughly speaking, the group \(S_N\) is thus acting on \(\mathcal{P}\) by permuting variables: A permutation \(\sigma \in S_N\) transforms a polynomial \(f\) by substituting \(x_{\sigma (i)}\) for each \(x_i\).

Note that this action of \(S_N\) on \(\mathcal{P}\) is a well-defined group action (as we will see in Proposition 6.3 below).

(c) A polynomial \(f \in \mathcal{P}\) is said to be symmetric if it satisfies

(d) We let \(\mathcal{S}\) be the set of all symmetric polynomials \(f \in \mathcal{P}\).

The \(\rho \) vector \((N{-}1, N{-}2, \ldots , 0)\) is itself an \(N\)-partition (since it is strictly decreasing, hence weakly decreasing).

The \(K\)-subalgebra \(\mathcal{S}\) of \(\mathcal{P}\) is called the ring of symmetric polynomials in \(N\) variables over \(K\).

The row partition \((n, 0, 0, \ldots , 0)\) with \(n\) boxes in the first row. This is the partition corresponding to \(h_n\). Requires \(N {\gt} 0\).

Convert an SSYT of row partition shape \((n, 0, \ldots , 0)\) back to a multiset: extract the entries of row \(0\) (which form a weakly increasing sequence of length \(n\)).

Let \(\lambda \) be an \(N\)-partition. We define the Schur polynomial \(s_{\lambda }\in \mathcal{P}\) by

The Schur polynomial \(s_\lambda \) is defined as \(s_\lambda = \sum _{T \in \mathrm{SSYT}(\lambda )} x_T\), where the sum is over all semistandard Young tableaux of shape \(\lambda \) with entries in \([N]\).

The cell bijection between two representations of skew Young diagrams. The first uses 0-indexed columns (\((i,j) \in Y(\lambda /\mu )\) iff \(\mu _i \le j {\lt} \lambda _i\)), and the second uses 1-indexed columns (\((i,j) \in Y(\lambda /\mu )\) iff \(\mu _i {\lt} j \le \lambda _i\)). The bijection is \((i, j) \mapsto (i, j+1)\).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions such that \(\mu \subseteq \lambda \). Then, we define the skew Young diagram \(Y\left( \lambda /\mu \right) \) to be the set difference

The filling bijection converts fillings between the two skew diagram representations by composing with the cell bijection.

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. We define the skew Schur polynomial \(s_{\lambda /\mu }\in \mathcal{P}\) by

The skew Schur polynomial \(s_{\lambda /\mu }\) is defined as \(s_{\lambda /\mu } = \sum _{T \in \mathrm{SSYT}(\lambda /\mu )} x_T\), where the sum is over all semistandard Young tableaux of skew shape \(\lambda /\mu \).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions.

A Young tableau \(T\) of shape \(\lambda /\mu \) is said to be semistandard if its entries

• increase weakly along each row (from left to right);

• increase strictly down each column (from top to bottom).

Formally speaking, this means that a Young tableau \(T:Y\left( \lambda /\mu \right) \rightarrow \left[ N\right] \) is semistandard if and only if

• we have \(T\left( i,j\right) \leq T\left( i,j+1\right) \) for any \(\left( i,j\right) \in Y\left( \lambda /\mu \right) \) satisfying \(\left( i,j+1\right) \in Y\left( \lambda /\mu \right) \);

• we have \(T\left( i,j\right) {\lt}T\left( i+1,j\right) \) for any \(\left( i,j\right) \in Y\left( \lambda /\mu \right) \) satisfying \(\left( i+1,j\right) \in Y\left( \lambda /\mu \right) \).

We let \(\operatorname *{SSYT}\left( \lambda /\mu \right) \) denote the set of all semistandard Young tableaux of shape \(\lambda /\mu \).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions such that \(\mu \subseteq \lambda \). A Young tableau of shape \(\lambda /\mu \) means a way of filling the boxes of \(Y\left( \lambda /\mu \right) \) with elements of \(\left[ N\right] \) (one element per box). Formally speaking, it is defined as a map \(T:Y\left( \lambda /\mu \right) \rightarrow \left[ N\right] \).

Young tableaux of shape \(\lambda /\mu \) are often called skew Young tableaux.

If we don’t have \(\mu \subseteq \lambda \), then we agree that there are no Young tableaux of shape \(\lambda /\mu \).

Let \(a=\left( a_{1},a_{2},\ldots ,a_{N}\right) \in \mathbb {N}^{N}\). Then:

(a) We let \(x^{a}\) denote the monomial \(x_{1}^{a_{1}}x_{2}^{a_{2}}\cdots x_{N}^{a_{N}}\).

(b) We let \(\operatorname *{sort}a\) mean the \(N\)-partition obtained from \(a\) by sorting the entries of \(a\) in weakly decreasing order.

For \(a = (a_1, a_2, \ldots , a_N) \in \mathbb {N}^N\), \(\operatorname {sort} a\) is the \(N\)-partition obtained by sorting the entries of \(a\) in weakly decreasing order.

For an \(N\)-partition \(\mu \), the sort preimage is the finite set

The bound \(a_i {\lt} |\mu | + 1\) makes the set finite (it is contained in \(\{ 0, \ldots , |\mu |\} ^N\)).

The finitely-supported version of \(\operatorname {sort}\): for a finitely-supported function \(d\) from \([N]\) to \(\mathbb {N}\), \(\operatorname {sortFinsupp}(d) = \operatorname {sort}(d)\), where \(d\) is viewed as a function \([N] \to \mathbb {N}\).

Let \(\lambda \) be an \(N\)-partition.

A Young tableau \(T\) of shape \(\lambda \) is said to be semistandard if its entries

• increase weakly along each row (from left to right);

• increase strictly down each column (from top to bottom).

Formally speaking, this means that a Young tableau \(T:Y\left( \lambda \right) \rightarrow \left[ N\right] \) is semistandard if and only if

• we have \(T\left( i,j\right) \leq T\left( i,j+1\right) \) for any \(\left( i,j\right) \in Y\left( \lambda \right) \) satisfying \(\left( i,j+1\right) \in Y\left( \lambda \right) \);

• we have \(T\left( i,j\right) {\lt}T\left( i+1,j\right) \) for any \(\left( i,j\right) \in Y\left( \lambda \right) \) satisfying \(\left( i+1,j\right) \in Y\left( \lambda \right) \).

We let \(\operatorname *{SSYT}\left( \lambda \right) \) denote the set of all semistandard Young tableaux of shape \(\lambda \).

An equivalence between the two SSYT representations in this project:

• The first uses a total function \(T : [N] \times \mathbb {N} \to [N]\) with a support condition (entries outside the diagram are \(0\)).

• The second uses a dependent function where the column index is bounded by the partition part: \(T(i, j)\) for \(j {\lt} \lambda _i\).

The equivalence converts between the total function and the bounded representations.

The inverse map of the nipat–SSYT bijection: given a skew SSYT \(T\) of shape \(\lambda /\mu \), construct the nipat \(\mathbf{p}(T)\) whose \(i\)-th path has east-step heights given by row \(i\) of \(T\).

The weakly increasing property of each path follows from row-weakness of \(T\). The column-strictness condition follows from column-strictness of non-adjacent rows in \(T\).

For a semistandard tableau \(T\) that is not \(\nu \)-Yamanouchi, define \(T^* = \operatorname {stemb}_\nu (T)\) as follows:

1. Let \(j\) be the largest violator column (where \(\nu + \operatorname {cont}(\operatorname {col}_{\geq j} T)\) is not a partition).

2. Let \(k\) be the smallest misstep index of \(\nu + \operatorname {cont}(\operatorname {col}_{\geq j} T)\).

3. Apply the prefix-restricted BK involution: \(T^* = \beta _k^{{\lt}j}(T)\).

Let \(T\) be a semistandard tableau and \(\nu \) an \(N\)-tuple. A positive integer \(j\) is a violator column if \(\nu + \operatorname {cont}(\operatorname {col}_{\geq j} T)\) is not an \(N\)-partition. An index \(k\) is a misstep for an \(N\)-tuple \(\alpha \) if \(k + 1 {\lt} N\) and \(\alpha _k {\lt} \alpha _{k+1}\) (i.e., the partition condition fails at \(k\)).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions.

(a) We write \(\lambda /\mu \) for the pair \(\left( \mu ,\lambda \right) \). Such a pair is called a skew partition.

(b) We say that \(\lambda /\mu \) is a horizontal strip if we have \(\mu \subseteq \lambda \) and the Young diagram \(Y\left( \lambda /\mu \right) \) has no two boxes lying in the same column.

(c) We say that \(\lambda /\mu \) is a vertical strip if we have \(\mu \subseteq \lambda \) and the Young diagram \(Y\left( \lambda /\mu \right) \) has no two boxes lying in the same row.

Now, let \(n\in \mathbb {N}\).

(d) We say that \(\lambda /\mu \) is a horizontal \(n\)-strip if \(\lambda /\mu \) is a horizontal strip and satisfies \(\left\vert Y\left( \lambda /\mu \right) \right\vert =n\).

(e) We say that \(\lambda /\mu \) is a vertical \(n\)-strip if \(\lambda /\mu \) is a vertical strip and satisfies \(\left\vert Y\left( \lambda /\mu \right) \right\vert =n\).

Convert a multiset \(s \in \mathrm{Sym}(\mathrm{Fin}\, N, n)\) to an SSYT of row partition shape \((n, 0, \ldots , 0)\): row \(0\) contains the sorted entries of \(s\), and all other rows are empty.

(a) We let \(\mathbf{0}\) denote the \(N\)-tuple \(\left( 0,0,\ldots ,0\right) \in \mathbb {N}^{N}\).

(b) Let \(\alpha =\left( \alpha _{1},\alpha _{2},\ldots ,\alpha _{N}\right) \) and \(\beta =\left( \beta _{1},\beta _{2},\ldots ,\beta _{N}\right) \) be two \(N\)-tuples in \(\mathbb {N}^{N}\). Then, we set

Note that \(\alpha +\beta \in \mathbb {N}^{N}\), whereas \(\alpha -\beta \in \mathbb {Z}^{N}\).

The finite set of \(N\)-partitions \(\lambda \) such that \(\lambda /\mu \) is a vertical \(n\)-strip. This is computed by filtering all functions bounded by the vertical strip constraints.

Let \(\lambda ,\mu ,\nu \) be three \(N\)-partitions. A semistandard tableau \(T\) of shape \(\lambda /\mu \) is said to be \(\nu \)-Yamanouchi (this is an adjective) if for each positive integer \(j\), the \(N\)-tuple \(\nu +\operatorname *{cont}\left( \operatorname {col}_{\geq j}T\right) \in \mathbb {N}^{N}\) is an \(N\)-partition (i.e., weakly decreasing).

Let \(\lambda \) be an \(N\)-partition.

The Young diagram of \(\lambda \) is defined as the set

We visually represent each element \(\left( i,j\right) \) of this Young diagram as a box in row \(i\) and column \(j\).

We denote the Young diagram of \(\lambda \) by \(Y\left( \lambda \right) \).

Let \(\lambda \) be an \(N\)-partition.

A Young tableau of shape \(\lambda \) means a way of filling the boxes of \(Y\left( \lambda \right) \) with elements of \(\left[ N\right] \) (one element per box). Formally speaking, it is defined as a map \(T:Y\left( \lambda \right) \rightarrow \left[ N\right] \).

Let \(\lambda \) and \(\mu \) be two \(N\)-partitions. If \(T\) is any Young tableau of shape \(\lambda /\mu \), then we define the corresponding monomial

Let \(\lambda \) be an \(N\)-partition. If \(T\) is any Young tableau of shape \(\lambda \), then we define the corresponding monomial

For \(i \in \mathbb {N}\), define the switch operation \(\operatorname {switch}_i\) on finite subsets \(S\) of \(\mathbb {N}\) by

In other words, if exactly one of \(i\) and \(i+1\) belongs to \(S\), then we replace it by the other; otherwise we leave \(S\) unchanged.

Let \(n\in \mathbb {N}\). Then, \(\binom {2n}{n}=\frac{1\cdot 3\cdot 5\cdot \cdots \cdot \left( 2n-1\right) }{n!}\cdot 2^{n}\).

For \(n,k\in \mathbb {N}\) with \(k \leq n\), we have \(\binom {n}{k}=\frac{n!}{k!\left( n-k\right) !}\).

For any \(n\in \mathbb {N}\), \(n!\) divides \(\left(\prod _{i=0}^{n-1}(2i+1)\right)\cdot 2^n\).

For any element \(r\) in a binomial ring and \(n \in \mathbb {N}\), \(n! \cdot \binom {r}{n} = r(r-1)(r-2)\cdots (r-n+1)\).

For natural numbers \(n, k\), the generalized binomial coefficient \(\binom {n}{k}\) (computed in any binomial ring) agrees with the natural-number binomial coefficient \(\binom {n}{k}\) as computed from Definition 1.1.

For any \(k\in \mathbb {N}\), we have \(\binom {-1}{k} = (-1)^k\).

For any \(r\), we have \(\binom {r}{1} = r\).

For natural numbers \(m, n\) with \(m {\gt} 0\) and \(n {\gt} 0\), we have \(\binom {m}{n}=\binom {m-1}{n-1}+\binom {m-1}{n}\).

For any element \(r\) in a binomial ring and \(k \in \mathbb {N}\), \(\binom {r+1}{k+1} = \binom {r}{k} + \binom {r}{k+1}\).

For any \(n\in \mathbb {N}\), \(\prod _{i=0}^{n-1}(2i+1) = (2n-1)!!\). That is, the product of odd numbers \(1\cdot 3\cdot 5\cdots (2n-1)\) equals the double factorial \((2n-1)!!\).

For any \(a, b \in \mathbb {N}\), we have \(\binom {a+b}{a} = \binom {a+b}{b}\).

For any binomial ring \(R\), natural numbers \(n, k\) with \(k \leq n\), \(\binom {n}{k} = \binom {n}{n-k}\) where \(n\) is viewed as an element of \(R\).

For \(k {\gt} 0\), we have \(\binom {0}{k} = 0\).

For any \(r\), we have \(\binom {r}{0} = 1\).

For \(d {\gt} 0\), the number of \(d\)-blocky \(k\)-element subsets of \(\{ 0, \ldots , n-1\} \) is

Let \(K\) be a field, \(d\) a positive integer, and \(\omega \) a primitive \(d\)-th root of unity. For \(n, k \in \mathbb {N}\),

Let \(n,d\in \mathbb {N}\). Then,

Let \(n,d\in \mathbb {N}\). Let \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\).

(a) If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right)\) is not all-even, then \(\sum _{\left( e_{1},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}} e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=0\).

(b) If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right)\) is all-even, then \(\sum _{\left( e_{1},\ldots ,e_{d}\right) \in \left\{ 1,-1\right\} ^{d}} e_{x_{1}}e_{x_{2}}\cdots e_{x_{n}}=2^{d}\).

Let \(n,d\in \mathbb {N}\). Let \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\). If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \) is not all-even, then

Let \(n,d\in \mathbb {N}\). Let \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \in \left[ d\right] ^{n}\). If the \(n\)-tuple \(\left( x_{1},x_{2},\ldots ,x_{n}\right) \) is all-even, then

Let \(n,d\in \mathbb {N}\). Let \(e = (e_1, \ldots , e_d) \in \{ 1,-1\} ^d\) and \(x = (x_1, \ldots , x_n) \in [d]^n\). For each \(k \in [d]\), let \(m_k\) be the multiplicity of \(k\) in \(x\). Then

For any \(k \in [d]\), the map \(\operatorname {flipSign}_k\) is an involution.

For any \(k \in [d]\) and \(e \in \{ 1,-1\} ^d\), we have \(\operatorname {flipSign}_k(e) \neq e\).

For any \(k, j \in [d]\) with \(j \neq k\) and \(e \in \{ 1,-1\} ^d\), \((\operatorname {flipSign}_k(e))_j = e_j\).

For any \(k \in [d]\) and \(e \in \{ 1,-1\} ^d\), \((\operatorname {flipSign}_k(e))_k = e_k + 1\) (in \(\mathbb {Z}/2\mathbb {Z}\)).

Let \(e \in \{ 1,-1\} ^d\), \(x \in [d]^n\), and \(k \in [d]\) such that the multiplicity \(m_k\) of \(k\) in \(x\) is odd. Then

For a sign tuple \(e \in \{ 1,-1\} ^d\), let \(S = \{ i \in [d] \mid e_i = -1\} \). Then

For a subset \(S \subseteq [d]\), the sign sum of the corresponding sign tuple is

There is a bijection between sign tuples \(\{ 1,-1\} ^d\) and subsets of \([d]\), sending each tuple \(e\) to the set \(S = \{ i \in [d] \mid e_i = -1\} \).

Let \(n,d\in \mathbb {N}\). Then

Let \(n,d\in \mathbb {N}\). Then

Let \(n,d\in \mathbb {N}\). Then

For any \(b \in \mathbb {Z}/2\mathbb {Z}\), we have \(\operatorname {toSign}(b+1) = -\operatorname {toSign}(b)\).

For any \(b \in \mathbb {Z}/2\mathbb {Z}\) and even \(m \in \mathbb {N}\), we have \((\operatorname {toSign} b)^m = 1\).

For any \(b \in \mathbb {Z}/2\mathbb {Z}\) and odd \(m \in \mathbb {N}\), we have \((\operatorname {toSign} b)^m = \operatorname {toSign} b\).

For any \(b \in \mathbb {Z}/2\mathbb {Z}\), we have \((\operatorname {toSign} b)^2 = 1\).

For \(n\in \mathbb {N}\), \(\binom {1/2}{n+1}\cdot (-4)^{n+1}\cdot (n+1) = -2\cdot \binom {2n}{n}\).

For \(n \geq 1\), \(c_n = \binom {2n}{n} - \binom {2n}{n-1}\).

For \(n\in \mathbb {N}\), \(\binom {1/2}{n+1}\cdot (-4)^{n+1} = -2\, c_n\).

For \(n\in \mathbb {N}\), \((n+1)\binom {1/2}{n+1} = \left(\frac{1}{2}-n\right)\binom {1/2}{n}\).

The explicit formula for Catalan numbers: \(c_n = \frac{1}{n+1}\binom {2n}{n}\).

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {Z}\), we have \(\left( n+m\right) a=na+ma\).

Let \(K\) be a commutative ring. For any \(a,b\in K\) and \(n\in \mathbb {N}\),

In a field \(F\), an element \(a\) is invertible if and only if \(a \neq 0\).

For an invertible element \(a\) and elements \(b, c \in L\), we have \(b / a = c\) if and only if \(b = c \cdot a\).

Let \(L\) be a commutative ring. If \(b\) and \(c\) are both inverses of \(a\), then \(b = c\). In other words, the inverse of an element (if it exists) is unique.

The definition of invertibility from Definition 1.63 is equivalent to the definition of a unit in Mathlib.

If \(a\) and \(b\) are invertible in \(L\), then \(a \cdot b\) is invertible.

Let \(K\) be a commutative ring. For any \(a,b\in K\) and \(n\in \mathbb {N}\), we have \(\left( ab\right) ^{n}=a^{n}b^{n}\).

Let \(K\) be a commutative ring. For any \(a,b,c\in K\), we have \(a\left( b-c\right) =\left( ab\right) -\left( ac\right)\).

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {Z}\), we have \(\left( nm\right) a=n\left( ma\right)\).

Let \(K\) be a commutative ring. For any \(a,b\in K\), we have \(-\left( a+b\right) =\left( -a\right) +\left( -b\right)\).

Let \(K\) be a commutative ring. For any \(a\in K\), we have \(-\left( -a\right) =a\).

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {N}\), we have \(a^{n+m}=a^{n}a^{m}\).

Let \(K\) be a commutative ring. For any \(a\in K\) and \(n,m\in \mathbb {N}\), we have \(a^{nm}=\left( a^{n}\right) ^{m}\).

Let \(K\) be a commutative ring. If \(S=\varnothing \), then \(\prod _{s\in S}a_{s}=1\).

Let \(K\) be a commutative ring. Let \(T\) be a finite set and \((a_s)_{s\in T}\), \((b_s)_{s\in T}\) be two families of elements of \(K\). Then \(\sum _{s\in T}\left( a_{s}+b_{s}\right) =\sum _{s\in T}a_{s}+\sum _{s\in T}b_{s}\).

Let \(K\) be a commutative ring. Let \(S\) be a finite type, and let \(X, Y\) be disjoint finite subsets of \(S\). For any family \((a_s)_{s \in S}\) of elements of \(K\), we have \(\sum _{s\in X\cup Y}a_{s}=\sum _{s\in X}a_{s}+\sum _{s\in Y}a_{s}\).

Let \(K\) be a commutative ring. If \(S=\varnothing \), then \(\sum _{s\in S}a_{s}=0\).

For an invertible element \(a\) and integers \(m, n \in \mathbb {Z}\), we have \(a^{m+n} = a^m \cdot a^n\).

For an invertible element \(a\) and a natural number \(n\), we have \(a^{-n} = (a^{-1})^n\). This defines negative integer powers.

The matrix \(F\) with entries \(F_{i,j} = x + d_i\, [i{=}j]\) decomposes as \(F = A + D\) where \(A\) is the \(n\times n\) constant matrix with all entries equal to \(x\) and \(D = \operatorname {diag}(d_1,\ldots ,d_n)\).

If the sign decomposition formula holds for \((P, Q', \sigma ')\) (where \(Q' = s_i(Q)\), \(\sigma ' = s_i\cdot \sigma \) for \(i\notin Q\), \(i{+}1\in Q\)), then it holds for \((P, Q, \sigma )\).

Let \(A\) and \(B\) be two finite sets. Let \(m\in \mathbb {N}\). Let \(f:A\rightarrow B\) be any map. Assume that each \(b\in B\) has exactly \(m\) preimages under \(f\) (that is, for each \(b\in B\), there are exactly \(m\) many elements \(a\in A\) such that \(f\left( a\right) =b\)). Then,

Let \(L\) be a commutative ring. Let \(a,u,v\in L\) be such that \(a\) is regular. Assume that \(au=av\). Then, \(u=v\).

Let \(l_1, l_2\) be lists such that \(l_1\) is a cyclic rotation of \(l_2\), and \(l_1\) has no duplicate entries. Then \(l_1\) and \(l_2\) give rise to the same cycle permutation.

Let \(l\) be a list with no duplicate entries, and let \(k \in \mathbb {N}\). Then the cycle permutation of \(l\) equals the cycle permutation of the \(k\)-fold rotation of \(l\).

Every element of the cycle lengths multiset is at least \(2\).

The sum of the cycle lengths (of nontrivial cycles) equals the number of non-fixed-point elements of \(\sigma \).

The parts of the cycle lengths partition sum to \(|X|\).

The minimum element of a cycle \(c\) belongs to the support of \(c\).

If \(x\) is not a fixed point of \(\sigma \) (i.e., \(\sigma (x) \neq x\)), then the cycle of \(\sigma \) containing \(x\) is among the cycles of \(\sigma \).

The product of the cycles of \(\sigma \) (in any order, since they commute) equals \(\sigma \).

The cycles of \(\sigma \) are pairwise disjoint, i.e., their supports are pairwise disjoint.

An element \(y\) appears in the flattened list of canonical cycle lists if and only if \(y\) is not a fixed point of \(\sigma \).

The flattened list of all canonical cycle lists has no duplicate entries.

If two cycles \(c\) and \(d\) are disjoint (as permutations), then their canonical lists are disjoint (as lists).

The cycle permutation determined by the canonical list equals \(c\).

The first element of the canonical list is minimal among all elements of the list.

The canonical list representation of a cycle has no duplicate entries.

Two permutations \(\sigma , \tau \) of a finite set \(X\) have the same cycle type (i.e., the same multiset of cycle lengths) if and only if they are conjugate, i.e., there exists a permutation \(g\) of \(X\) such that \(\tau = g \sigma g^{-1}\).

The product of the cycle permutations of the canonical list representations of \(\sigma \)’s cycles equals \(\sigma \).

For \(n\times n\)-matrices \(A\) and \(B\),

Swapping summation order:

Partitioning by \(Q = \sigma (P)\):

Let \(A \in K^{n \times n}\) with \(n \geq 2\). Then

Let \(A\) be an \(n \times n\) matrix with \(\det A\) a unit. Then for any index functions \(f\) and \(g\),

That is, the adjugate submatrix equals \(\det A\) times the corresponding inverse submatrix.

Let \(M = \begin{pmatrix} A & B \\ C & D \end{pmatrix}\) be an invertible block matrix with \(D\) invertible and Schur complement \(A - BD^{-1}C\) invertible. Let \(k = |A|\) (the size of the top-left block) with \(k \geq 1\). Then

Let \(K\) be a field. Let \(x_1, \ldots , x_m, y_1, \ldots , y_m \in K\) with \(x_i + y_j \neq 0\) for all \(i, j\). Then

Let \(n \in \mathbb {N}\). Let \(x_1, \ldots , x_n \in R\) and \(y_1, \ldots , y_n \in R\) be elements of a commutative ring \(R\). Then

This is equivalent to the Cauchy determinant formula after dividing both sides by \(\prod _{(i,j) \in [n]^2} (x_i + y_j)\).

Let \(C(m)\) be the \(m \times m\) matrix with entry \((i,j) = \prod _{k \neq j}(X_i + Y_k)\) over \(\mathbb {Z}[X_1, \ldots , X_m, Y_1, \ldots , Y_m]\). For distinct \(i, j\), we have \((X_i - X_j) \mid \det (C(m))\).

For distinct \(i, j\), we have \((Y_i - Y_j) \mid \det (C(m))\), where \(C(m)\) is the polynomial Cauchy matrix from Lemma 5.117.

Let \(A\in K^{n\times m}\), \(B\in K^{m\times n}\), and let \(f\colon [n]\to [m]\) be a non-injective function. Then

For a fixed \(n\)-element subset \(S\subseteq [m]\),

where \(S_k\) denotes the \(k\)-th element of \(S\) in sorted order.

For a block matrix \(M = \begin{pmatrix} A & B \\ C & D \end{pmatrix}\) with \(D\) invertible and the Schur complement \(A - BD^{-1}C\) invertible, we have

Let \(K\) be a field. Let \(A \in K^{m \times m}\) be an invertible matrix. Let \(P, Q \subseteq [m]\) with \(|P| = |Q|\). Then

For \(n \geq 2\), a matrix with all entries equal to \(c\) has determinant \(0\). This is a corollary of Proposition 5.12 with \(x_i = 1\) and \(y_j = c\).

For a singleton \(P = \{ p\} \), the \(1\times 1\) submatrix of the constant-\(x\) matrix has determinant \(x\).

Let \(A\) be the \(n\times n\) constant matrix with all entries equal to \(x\). If \(P\subseteq [n]\) has \(|P| \ge 2\), then \(\det (\operatorname {sub}_P^P A) = 0\).

The Desnanot–Jacobi identity holds for \(2 \times 2\) matrices by direct computation.

Let \(A\) be an \(m \times m\) matrix with \(\det A\) a unit. Let \(P, Q \subseteq [m]\) with \(|P| = |Q| = k\). Then

This reduces Jacobi’s complementary minor theorem to the complementary minor theorem for inverse matrices.

Let \(A \in K^{m \times m}\) and \(f, g : [n] \xrightarrow {\sim } [m]\) be bijections. Then

For \(n \geq 3\), the factor matrix \(A\) has determinant \(0\).

The determinant of a diagonal matrix equals the product of its diagonal entries: \(\det (\mathrm{diag}(d_1, \ldots , d_n)) = d_1 d_2 \cdots d_n\).

The determinant of a \(1 \times 1\) matrix is its single entry: \(\det (a) = a\).

The determinant of a \(2 \times 2\) matrix satisfies \(\det \begin{pmatrix} a & b \\ c & d \end{pmatrix} = ad - bc\).

The determinant of a \(0 \times 0\) matrix is \(1\) (empty product convention).

Let \(A\) be a \(5 \times 5\) matrix such that \(A_{i,j} = 0\) whenever \(i, j \in \{ 2, 3, 4\} \). Then \(\det A = 0\). This formalizes the \(5 \times 5\) hollow matrix example: a matrix with a \(3 \times 3\) block of zeros in the middle has determinant \(0\).

The image of a finset under a permutation has the same cardinality: \(|\sigma (P)| = |P|\).

The image of a complement equals the complement of the image: \(\sigma (P^c) = \sigma (P)^c\).

If \(\sigma (P) = Q\), then \(\sigma ^{-1}(Q) = P\).

Let \(K\) be a field and \(A \in K^{n \times n}\) with \(\det A \neq 0\). Then for all \(i, j\),

Let \(K\) be a field, \(A \in K^{m \times m}\) with \(\det A \neq 0\), and \(\sigma , \tau \) bijections from \([n]\) to \([m]\). Then

where subscripts denote the submatrix obtained by reindexing rows and columns via the given bijections.

For a \(2 \times 2\) matrix \(A\), the \(2 \times 2\) determinant of the corner entries of \(\operatorname {adj} A\) satisfies

This is the base case of the Jacobi complementary minor theorem (since \(\det (A') = 1\) for the \(0 \times 0\) inner submatrix).

For a \(3 \times 3\) matrix \(A\), the \(2 \times 2\) determinant of the corner entries of \(\operatorname {adj} A\) at positions \(\{ 0, 2\} \times \{ 0, 2\} \) satisfies

This verifies the Jacobi complementary minor theorem for \(3 \times 3\) matrices with \(P = Q = \{ 0, 2\} \).

Let \(K\) be a field. Let \(A \in K^{m \times m}\) with \(\det A \neq 0\). Let \(P, Q \subseteq [m]\) with \(|P| = |Q| \geq 1\). Then

Let \(n\in \mathbb {N}\). Let \(d_1,d_2,\ldots ,d_n\in K\). Let

(a) We have \(\det (\operatorname {sub}_P^P D) = \prod _{i\in P} d_i\) for any subset \(P\) of \([n]\).

(b) Let \(P\) and \(Q\) be two distinct subsets of \([n]\) satisfying \(|P|=|Q|\). Then, \(\det (\operatorname {sub}_P^Q D) = 0\).

The determinant of the identity matrix is \(1\): \(\det I_n = 1\).

If \(|P| \neq |Q|\), then no permutation maps \(P\) to \(Q\): \(\mathrm{permsMapping}(P, Q) = \emptyset \).

When \(|P| = |Q|\), the submatrix determinant equals the actual determinant of the submatrix \(A[P, Q]\).

When \(|P| \neq |Q|\), the submatrix determinant is \(0\).

The submatrix determinant of the empty row and column sets is \(1\): \(\mathrm{submatrixDet}(A, \emptyset , \emptyset ) = 1\).

Let \(A\) be an \((m+2) \times (m+2)\) matrix, and let \(p {\lt} q\) and \(u {\lt} v\) be indices. Then

where the right-hand side uses the complement-based submatrix construction. This connects the explicit order-preserving injection used in the submatrix construction to the general complement-based definition, enabling the use of Jacobi’s complementary minor theorem.

Let \(n \geq 2\). Then,

For \(n \geq 2\), the matrix \((x_i + y_j)_{i,j}\) factors as \(A \cdot B\) where:

The factor matrix \(A\) in the factorization of the sum matrix \((x_i + y_j)\) has a zero column (column index \(2\)) when \(n \geq 3\). The matrix \(A\) has \(x_i\) in the first column, \(1\) in the second column, and \(0\) elsewhere.

For fixed subsets \(P,Q\subseteq [n]\) with \(|P|=|Q|\):

Let \(n \in \mathbb {N}\). Consider the polynomial ring \(\mathbb {Z}[x_1, x_2, \ldots , x_n]\) in \(n\) indeterminates \(x_1, x_2, \ldots , x_n\) with integer coefficients. In this ring, we have

Let \(A\) be an \(m \times m\) matrix and \(\sigma \) a permutation of \([m]\). Then \(\det (A \circ \sigma ) = \operatorname {sign}(\sigma ) \cdot \det A\), where \(A \circ \sigma \) denotes the column permutation \(A_{i,\sigma (j)}\).

The determinant of the polynomial Vandermonde matrix (with entries \(x_i^{m-1-j}\)) equals

where \(\tau \) is the column reversal permutation (sending \(j\) to \(m - 1 - j\)). This relates the textbook matrix convention to Mathlib’s via column reversal.

Let \(v_1, \ldots , v_m\) be elements of a commutative ring \(S\). Then

The sign of the column reversal permutation \(\tau \) on \(\{ 1, 2, \ldots , m\} \) (sending \(j\) to \(m + 1 - j\)) satisfies

Let \(R\) be an integral domain, and let \(P \in R[x_0, x_1, \ldots , x_{m+1}]\). If \(P\) vanishes when \(x_0\) is replaced by \(x_1\) (i.e., \(P|_{x_0 = x_1} = 0\)), then \((x_0 - x_1) \mid P\).

Let \(p \in R[x_1, \ldots , x_n]\) be a multivariate polynomial and \(i \neq j\). Then \((x_i - x_j) \mid p - p|_{x_i = x_j}\), where \(p|_{x_i = x_j}\) denotes the substitution of \(x_j\) for \(x_i\).

For distinct variables \(x_i, x_j\) in \(\mathbb {Z}[x_1, \ldots , x_n]\), the polynomial \(x_i - x_j\) is irreducible.

For distinct \(i, j\), the polynomial \(x_i - x_j \in \mathbb {Z}[x_1, \ldots , x_n]\) is primitive (its content is \(1\)).

Let \(i \neq j\) and \(k \neq l\) be pairs of distinct indices such that \(\{ i,j\} \) and \(\{ k,l\} \) are not equal as unordered pairs. Then \((x_i - x_j)\) and \((x_k - x_l)\) are coprime in \(\mathbb {Z}[x_1, \ldots , x_n]\).

For distinct \(i, j\), the total degree of \(x_i - x_j\) in \(\mathbb {Z}[x_1, \ldots , x_n]\) is \(1\).

For \(n \geq 1\), the determinant of the zero matrix is \(0\). (For \(n = 0\), the zero matrix is the empty matrix, and \(\det (\emptyset ) = 1\).)

Let \(T\) be a tiling of \(R_{n,3}\) with \(n \ge 2\) that has a vertical domino in the top two squares of column \(1\). Then \(T\) contains the basement domino \(\{ (1,1),(2,1)\} \).

Let \(T\) be a faultfree tiling of \(R_{n,3}\) that has a vertical domino in the top two squares of column \(1\). For each positive integer \(i {\lt} n/2\), the tiling \(T\) contains:

• the basement domino \(\left\{ (2i-1,\, 1),\, (2i,\, 1)\right\} \),

• the middle domino \(\left\{ (2i,\, 2),\, (2i+1,\, 2)\right\} \),

• the top domino \(\left\{ (2i,\, 3),\, (2i+1,\, 3)\right\} \).

Let \(T\) be a faultfree tiling of \(R_{n,3}\) that has a vertical domino in the top two squares of column \(1\). Then \(n\) is even.

If \(T\) is a faultfree tiling of \(R_{n,3}\) with a vertical domino in the top two squares of column \(1\), then \(n\) is even and \(T = A_n\).

If \(T\) is a faultfree tiling of \(R_{n,3}\) with a vertical domino in the bottom two squares of column \(1\), then \(n\) is even and \(T = B_n\).

If \(T\) is a faultfree tiling of \(R_{2,3}\) with no vertical domino in column \(1\), then \(T = C\).

If a domino \(d\) in a tiling of \(R_{n+2,2}\) contains \((1,1)\), then either \(d\) is the vertical domino \(\{ (1,1),(1,2)\} \) or \(d\) is the horizontal domino \(\{ (1,1),(2,1)\} \).

For any tiling \(T\) of \(R_{n+1,2}\) (with \(n + 1 \ge 1\)), there exists a domino \(d \in T\) that covers the cell \((1,1)\).

If a tiling \(T\) of \(R_{n+2,2}\) contains a horizontal domino \(d\) with \((1,1) \in d\), then \(T\) also contains a domino \(d'\) with \(d' = \{ (1,2),(2,2)\} \).

If \(T\) is a faultfree tiling of \(R_{n,3}\) with a vertical domino in the top two squares of column \(1\), then \(n \ge 2\).

If a tiling \(T\) of \(R_{n,3}\) has a vertical domino in the top two squares of some column \(c\), then \(n \ge c\).

Every tiling \(T\) of \(R_{n+2,2}\) either has a “vertical first column” (a domino with cells \(\{ (1,1),(1,2)\} \)) or has a “horizontal pair” (two dominos with cells \(\{ (1,1),(2,1)\} \) and \(\{ (1,2),(2,2)\} \)).

If \(T\) is a faultfree tiling of \(R_{n,3}\) with \(n \ge 1\) and no vertical domino in column \(1\), then \(n = 2\).

If \(R_{n,3}\) admits a domino tiling, then \(n\) is even (or \(n = 0\)).

Given a tiling \(T\) of \(R_{n,2}\), prepending the two horizontal dominos \(\{ (1,1),(2,1)\} \) and \(\{ (1,2),(2,2)\} \) and shifting all of \(T\)’s dominos right by \(2\) gives a valid tiling of \(R_{n+2,2}\).

Given a tiling \(T\) of \(R_{n,2}\), prepending the vertical domino \(\{ (1,1),(1,2)\} \) and shifting all of \(T\)’s dominos right by \(1\) gives a valid tiling of \(R_{n+1,2}\).

The \(\mathbb {N}\)-based rectangle \(\{ (i,j) \mid 1 \le i \le n, 1 \le j \le m\} \) and the \(\mathbb {Z}\)-based rectangle \(\{ (i,j) \in \mathbb {Z}^2 \mid 1 \le i \le n, 1 \le j \le m\} \) are in bijection via the coordinate casting map.

If \(T\) is a faultfree tiling of \(R_{n,3}\), then its horizontal reflection is also faultfree.

Reflecting a tiling of \(R_{n,3}\) twice yields the original tiling.

The reflection of a tiling preserves the minimum and maximum column of each domino: for every domino \(d\) in \(T\) and its reflected image \(d'\), the minimum column of \(d'\) equals that of \(d\), and the maximum column of \(d'\) equals that of \(d\).

If two tilings \(T_1\) and \(T_2\) of \(R_{n,3}\) are equal, then their reflections are also equal.

A tiling \(T\) of \(R_{n,3}\) has a vertical domino in the top two squares of column \(c\) if and only if its reflection has a vertical domino in the bottom two squares of column \(c\) (and vice versa).

Given a tiling \(T\) of \(R_{n+2,2}\) that contains both horizontal dominos \(\{ (1,1),(2,1)\} \) and \(\{ (1,2),(2,2)\} \), removing them and shifting all other dominos left by \(2\) gives a valid tiling of \(R_{n,2}\).

Given a tiling \(T\) of \(R_{n+1,2}\) that contains the vertical domino \(\{ (1,1),(1,2)\} \), removing it and shifting all other dominos left by \(1\) gives a valid tiling of \(R_{n,2}\).

The map from \(\mathrm{Tiling}(R_{n,2}) \sqcup \mathrm{Tiling}(R_{n+1,2})\) to \(\mathrm{Tiling}(R_{n+2,2})\) given by prepending the appropriate dominos is surjective: for every tiling \(T\) of \(R_{n+2,2}\), there exists an element \(x\) of \(\mathrm{Tiling}(R_{n,2}) \sqcup \mathrm{Tiling}(R_{n+1,2})\) whose prepended image equals \(T\).

For every tiling \(T\) of \(R_{n+2,2}\), classifying \(T\) by its first-column structure (vertical or horizontal pair), restricting, and then prepending recovers \(T\).

For every \(x \in \mathrm{Tiling}(R_{n,2}) \sqcup \mathrm{Tiling}(R_{n+1,2})\), classifying the prepended tiling by its first-column structure and then restricting recovers \(x\). This shows that the prepending map is injective and the classification map is surjective.

For each even \(n \ge 2\), the tiling \(A_n\) is faultfree. The basement dominos prevent faults between columns \(2i-1\) and \(2i\), while the middle and top dominos prevent faults between columns \(2i\) and \(2i+1\).

For each even \(n \ge 2\), the tiling \(A_n\) has a vertical domino in the top two squares of column \(1\), namely the left wall \(\{ (1,2),(1,3)\} \).

For each even \(n \ge 2\), \(B_n\) equals the reflection of \(A_n\).

For each even \(n \ge 2\), the tiling \(B_n\) is faultfree.

For each even \(n \ge 2\), the tiling \(B_n\) has a vertical domino in the bottom two squares of column \(1\), namely the left wall \(\{ (1,1),(1,2)\} \) of \(B_n\).

The tiling \(C\) is faultfree.

The tiling \(C\) has no vertical domino in column \(1\). All three dominos of \(C\) are horizontal.

If a set of natural-number-based dominos covers the natural-number-based rectangle \(R_{n,m}\), then their images under the coordinate casting cover the \(\mathbb {Z}\)-based rectangle \(R_{n,m}\).

If a set of natural-number-based dominos is pairwise disjoint, then their images under the coordinate casting are also pairwise disjoint.

If a tiling \(T\) of \(R_{n,3}\) has a vertical domino in column \(1\), then either \(T\) has a vertical domino in the top two squares of column \(1\) (rows \(2\)–\(3\)), or \(T\) has a vertical domino in the bottom two squares of column \(1\) (rows \(1\)–\(2\)).

For \(\sigma \) with \(\sigma (P) = Q\):

1. \(\sigma (p_j) = q_{\alpha _\sigma (j)}\) for all \(j\),

2. \(\sigma (p'_j) = q'_{\beta _\sigma (j)}\) for all \(j\).

For each \(m\in \mathbb {N}\),

The family \(\left(1+x^{2^{i}}\right)_{i\in \mathbb {N}}\) is multipliable.

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

The coefficient of \(x^k\) in \(f(n)\cdot g(n)\) equals

Let \(n\in \mathbb {N}\). Let \(\left(p_{i,k}\right)\) be a family indexed by \(\{ 1,2,\ldots ,n\} \times S_i\), and let \(f\) be a choice function selecting \(f(i) \in S_i\) for each \(i\). If for some \(j\in \{ 1,2,\ldots ,n\} \), the FPS \(p_{j,f(j)}\) satisfies \([x^m](p_{j,f(j)}) = 0\) for all \(m\le d\), then \([x^d]\left(\prod _{i} p_{i,f(i)}\right) = 0\).

The coefficient \([x^k](1+x)^c\) equals the evaluation of a polynomial in \(c\):

for some \(q_k\in \mathbb {Q}[x]\).

For natural \(N\ge 1\) and \(m\in \mathbb {N}\),

For \(k {\lt} m\), we have \([x^k](\overline{\log }^m) = 0\) (since \(\overline{\log }\) has order \(\geq 1\), so \(\overline{\log }^m\) has order \(\geq m\)).