A.5 Details on Laurent power series

Fix a commutative ring \(K\).

A.5.1 Proof of Theorem 1.498 (sketched)

The set \(K\left[x^{\pm }\right]\) is closed under addition, scaling, and the convolution product from Definition 1.497 (analogous to Theorem 1.148, replacing \(\sum _{i=0}^{n}\) sums by \(\sum _{i \in \mathbb {Z}}\) sums). The multiplication is associative, commutative, distributive, and \(K\)-bilinear (analogous to the corresponding parts of Theorem 1.76). The element \(\left(\delta _{i,0}\right)_{i \in \mathbb {Z}}\) is a neutral element for multiplication.

It remains to show that \(x\) is invertible. Set \(\overline{x} := \left(\delta _{i,-1}\right)_{i \in \mathbb {Z}}\). Then \(x \overline{x} = 1\) and \(\overline{x} x = 1\) by direct calculation. For example, from \(x = \left(\delta _{i,1}\right)_{i \in \mathbb {Z}}\) and \(\overline{x} = \left(\delta _{i,-1}\right)_{i \in \mathbb {Z}}\), we get

\[ x \overline{x} = \left(c_n\right)_{n \in \mathbb {Z}}, \quad \text{where} \quad c_n = \sum _{i \in \mathbb {Z}} \delta _{i,1}\, \delta _{n-i,-1} \]

(by Definition 1.497). For each \(n \in \mathbb {Z}\),

\begin{align*} c_n & = \sum _{i \in \mathbb {Z}} \delta _{i,1}\, \delta _{n-i,-1} = \underbrace{\delta _{1,1}}_{= 1} \delta _{n-1,-1} + \sum _{\substack{[i, , \in , \mathbb , {, Z, }, , \\ , , i, , \neq , 1]}} \underbrace{\delta _{i,1}}_{= 0\text{ (since } i \neq 1\text{)}} \delta _{n-i,-1} \\ & = \delta _{n-1,-1} = \delta _{n,0}, \end{align*}

since \(n - 1 = -1\) if and only if \(n = 0\). Hence \(x \overline{x} = \left(\delta _{n,0}\right)_{n \in \mathbb {Z}} = 1\). The proof of \(\overline{x} x = 1\) is analogous, or follows by commutativity.

A.5.2 Helpers for Theorem 1.498

Lemma A.107 \(T(1) \cdot T(-1) = 1\)

✓

In the Laurent polynomial ring, \(T(1) \cdot T(-1) = 1\). This witnesses the right inverse of \(x\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_inv {K : Type u_1} [CommRing K] :

LaurentPolynomial.T 1 * LaurentPolynomial.T (-1) = 1

Proof ▶

Follows from \(T(a) \cdot T(b) = T(a+b)\) with \(a = 1\), \(b = -1\).

Lemma A.108 \(T(-1) \cdot T(1) = 1\)

✓

In the Laurent polynomial ring, \(T(-1) \cdot T(1) = 1\). This witnesses the left inverse of \(x\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_neg_one_mul_T {K : Type u_1} [CommRing K] :

LaurentPolynomial.T (-1) * LaurentPolynomial.T 1 = 1

Proof ▶

Follows from \(T(a) \cdot T(b) = T(a+b)\) with \(a = -1\), \(b = 1\).

A.5.3 Multiplication by \(x\) shifts coefficients

Lemma A.109 Multiplication by \(x\) and \(x^{-1}\) shifts coefficients

Let \(\mathbf{a} = \left(a_n\right)_{n \in \mathbb {Z}}\) be a Laurent polynomial in \(K\left[x^{\pm }\right]\). Then,

\[ x \cdot \mathbf{a} = \left(a_{n-1}\right)_{n \in \mathbb {Z}} \qquad \text{and} \qquad x^{-1} \cdot \mathbf{a} = \left(a_{n+1}\right)_{n \in \mathbb {Z}}. \]

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_mul_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) :

(LaurentPolynomial.T 1 * a) n = a (n - 1)

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_neg_one_mul_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) :

(LaurentPolynomial.T (-1) * a) n = a (n + 1)

Proof ▶

From \(x = \left(\delta _{i,1}\right)_{i \in \mathbb {Z}}\) and \(\mathbf{a} = \left(a_i\right)_{i \in \mathbb {Z}}\), we obtain

\[ x \cdot \mathbf{a} = \left(\delta _{i,1}\right)_{i \in \mathbb {Z}} \cdot \left(a_i\right)_{i \in \mathbb {Z}} = \left(c_n\right)_{n \in \mathbb {Z}}, \quad \text{where} \quad c_n = \sum _{i \in \mathbb {Z}} \delta _{i,1}\, a_{n-i} \]

(by Definition 1.497). For each \(n \in \mathbb {Z}\),

\begin{align*} c_n & = \sum _{i \in \mathbb {Z}} \delta _{i,1}\, a_{n-i} = \underbrace{\delta _{1,1}}_{= 1} a_{n-1} + \sum _{\substack{[i, , \in , \mathbb , {, Z, }, , \\ , , i, , \neq , 1]}} \underbrace{\delta _{i,1}}_{= 0\text{ (since } i \neq 1\text{)}} a_{n-i} \\ & = a_{n-1}. \end{align*}

Thus, \(x \cdot \mathbf{a} = \left(a_{n-1}\right)_{n \in \mathbb {Z}}\).

It remains to prove that \(x^{-1} \cdot \mathbf{a} = \left(a_{n+1}\right)_{n \in \mathbb {Z}}\). Let \(\mathbf{b} = \left(a_{n+1}\right)_{n \in \mathbb {Z}}\); this is again a Laurent polynomial in \(K\left[x^{\pm }\right]\). Applying the result just proved to \(\mathbf{b}\) (with \(a_{n+1}\) in place of \(a_n\)) yields

\[ x \cdot \mathbf{b} = \left(a_{(n-1)+1}\right)_{n \in \mathbb {Z}} = \left(a_n\right)_{n \in \mathbb {Z}} = \mathbf{a}. \]

Dividing by the invertible element \(x\), we get \(\mathbf{b} = x^{-1} \cdot \mathbf{a}\), i.e. \(x^{-1} \cdot \mathbf{a} = \left(a_{n+1}\right)_{n \in \mathbb {Z}}\).

Lemma A.110 Multiplication on the right by \(T\) shifts coefficients

For any Laurent polynomial \(\mathbf{a}\),

\[ \mathbf{a} \cdot x = \left(a_{n-1}\right)_{n \in \mathbb {Z}} \qquad \text{and} \qquad \mathbf{a} \cdot x^{-1} = \left(a_{n+1}\right)_{n \in \mathbb {Z}}. \]

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.mul_T_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) :

(a * LaurentPolynomial.T 1) n = a (n - 1)

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.mul_T_neg_one_coeff {K : Type u_1} [CommRing K] (a : LaurentPolynomial K) (n : ℤ) :

(a * LaurentPolynomial.T (-1)) n = a (n + 1)

Proof ▶

Follows from Lemma A.109 by commutativity of multiplication.

A.5.4 Powers of \(x\)

Lemma A.111 \(T(m) \cdot T(n) = T(m + n)\)

✓

For all \(m, n \in \mathbb {Z}\), we have \(T(m) \cdot T(n) = T(m + n)\) in the Laurent polynomial ring. This is the fundamental multiplicative law for Laurent monomials.

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_mul_T {K : Type u_1} [CommRing K] (m n : ℤ) :

LaurentPolynomial.T m * LaurentPolynomial.T n = LaurentPolynomial.T (m + n)

Proof ▶

This is the group homomorphism property of \(T\): \(T(a) \cdot T(b) = T(a+b)\).

Lemma A.112 \(T(1)^n = T(n)\) for natural numbers

✓

For any natural number \(n\), we have \(T(1)^n = T(n)\) in the Laurent polynomial ring.

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_one_pow {K : Type u_1} [CommRing K] (n : ℕ) :

LaurentPolynomial.T 1 ^ n = LaurentPolynomial.T ↑n

Proof ▶

Follows from \(T(1)^n = T(1 \cdot n) = T(n)\) by the group homomorphism property.

Proposition A.113 \(x^k = (\delta _{i,k})_{i \in \mathbb {Z}}\) for all \(k \in \mathbb {Z}\)

We have

\[ x^k = \left(\delta _{i,k}\right)_{i \in \mathbb {Z}} \qquad \text{for each } k \in \mathbb {Z}. \]

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_coeff_eq {K : Type u_1} [CommRing K] (k i : ℤ) :

(LaurentPolynomial.T k) i = if i = k then 1 else 0

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_one_zpow {K : Type u_1} [CommRing K] (k : ℤ) :

↑(⋯.unit ^ k) = LaurentPolynomial.T k

Proof ▶

This is proved by two-sided induction on \(k\) (see [ Grinbe15 ] , §2.15 for a detailed explanation of two-sided induction).

Base case (\(k = 0\)): \(x^0 = 1 = \left(\delta _{i,0}\right)_{i \in \mathbb {Z}}\), which is the definition of the unity element.

Induction step from \(k\) to \(k+1\): Assume \(x^k = \left(\delta _{i,k}\right)_{i \in \mathbb {Z}}\). By Lemma A.109 (the \(x \cdot \mathbf{a} = \left(a_{n-1}\right)_{n \in \mathbb {Z}}\) part),

\[ x^{k+1} = x \cdot x^k = x \cdot \left(\delta _{i,k}\right)_{i \in \mathbb {Z}} = \left(\delta _{n-1,k}\right)_{n \in \mathbb {Z}} = \left(\delta _{n,k+1}\right)_{n \in \mathbb {Z}}, \]

since \(n - 1 = k\) if and only if \(n = k + 1\).

Induction step from \(k\) to \(k-1\): Assume \(x^k = \left(\delta _{i,k}\right)_{i \in \mathbb {Z}}\). By Lemma A.109 (the \(x^{-1} \cdot \mathbf{a} = \left(a_{n+1}\right)_{n \in \mathbb {Z}}\) part),

\[ x^{k-1} = x^{-1} \cdot x^k = x^{-1} \cdot \left(\delta _{i,k}\right)_{i \in \mathbb {Z}} = \left(\delta _{n+1,k}\right)_{n \in \mathbb {Z}} = \left(\delta _{n,k-1}\right)_{n \in \mathbb {Z}}, \]

since \(n + 1 = k\) if and only if \(n = k - 1\).

Lemma A.114 Coefficient of \(x^k\)

✓

For all \(k, i \in \mathbb {Z}\), the coefficient of \(x^k\) at position \(i\) is \(\delta _{i,k}\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.T_one_zpow_coeff {K : Type u_1} [CommRing K] (k i : ℤ) :

↑(⋯.unit ^ k) i = if i = k then 1 else 0

Proof ▶

Immediate from Proposition A.113.

A.5.5 Proof of Proposition 1.505 (sketched)

Definition A.115 Summable family of monomials

✓

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.

docs source

def AlgebraicCombinatorics.FPS.Laurent.singleFamily {K : Type u_1} [CommRing K] (x : LaurentSeries K) :

HahnSeries.SummableFamily ℤ K ↑(HahnSeries.support x)

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

Lemma A.116 Coefficient of a Laurent series as a finitary sum

For any Laurent series \(\mathbf{a} = (a_n)_{n \in \mathbb {Z}}\) and any \(n \in \mathbb {Z}\), the \(n\)-th coefficient satisfies

\[ a_n = \sum _{i \in \operatorname {supp}(\mathbf{a})}^{\mathrm{fin}} [x^n](a_i \cdot x^i). \]

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.laurentSeries_coeff_eq_finsum_single {K : Type u_1} [CommRing K] (x : LaurentSeries K) (n : ℤ) :

x.coeff n = ∑ᶠ (i : ↑(HahnSeries.support x)), ((HahnSeries.single ↑i) (x.coeff ↑i)).coeff n

Proof ▶

Follows by rewriting the left-hand side as the sum of its monomial components and extracting the coefficient.

Proposition 1.505 follows: any Laurent polynomial \(\mathbf{a} = (a_i)_{i \in \mathbb {Z}}\) satisfies \(\mathbf{a} = \sum _{i \in \mathbb {Z}} a_i x^i\), analogously to Corollary 1.85 but using Proposition A.113 instead of Proposition 1.84.

A.5.6 Proof of Theorem 1.509 (sketched)

The proof is analogous to Theorem 1.498. The only different piece is the proof that \(K\left(\left(x\right)\right)\) is closed under multiplication.

Let \(\left(a_n\right)_{n \in \mathbb {Z}}\) and \(\left(b_n\right)_{n \in \mathbb {Z}}\) be two elements of \(K\left(\left(x\right)\right)\). Their product is

\[ \left(a_n\right)_{n \in \mathbb {Z}} \cdot \left(b_n\right)_{n \in \mathbb {Z}} = \left(c_n\right)_{n \in \mathbb {Z}}, \quad \text{where} \quad c_n = \sum _{i \in \mathbb {Z}} a_i\, b_{n-i}. \]

We must show that \(\left(c_{-1}, c_{-2}, c_{-3}, \ldots \right)\) is essentially finite.

Since \(\left(a_n\right) \in K\left(\left(x\right)\right)\), there exists a negative integer \(p\) such that \(a_i = 0\) for all \(i \le p\). Similarly, there exists a negative integer \(q\) such that \(b_j = 0\) for all \(j \le q\). Set \(r := p + q\). For any integer \(n \le r\):

Each \(i \ge p\) satisfies \(n - i \le r - p = q\), hence \(b_{n-i} = 0\).
Each \(i {\lt} p\) satisfies \(a_i = 0\).

Therefore

\[ c_n = \sum _{i \in \mathbb {Z}} a_i\, b_{n-i} = \sum _{\substack{[i, , \in , \mathbb , {, Z, }, , \\ , , i, , {\lt}, , p]}} \underbrace{a_i}_{= 0} b_{n-i} + \sum _{\substack{[i, , \in , \mathbb , {, Z, }, , \\ , , i, , \ge , p]}} a_i \underbrace{b_{n-i}}_{= 0} = 0. \]

Hence all \(n \le r\) satisfy \(c_n = 0\), so the sequence \(\left(c_{-1}, c_{-2}, \ldots \right)\) is essentially finite.

A.5.7 Helpers for the embeddings

Lemma A.117 Power series coefficient preservation

✓

The embedding \(K[\! [x]\! ] \hookrightarrow K(\! (x)\! )\) preserves coefficients: for any power series \(f\) and any \(n \in \mathbb {N}\), the \(n\)-th coefficient of the image equals the \(n\)-th coefficient of \(f\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.coeff_powerSeriesToLaurent {K : Type u_1} [CommRing K] (f : PowerSeries K) (n : ℕ) :

(powerSeriesToLaurent f).coeff ↑n = (PowerSeries.coeff n) f

Proof ▶

This is a standard result relating power series to Laurent series: the embedding preserves coefficients.

Lemma A.118 Laurent polynomial embedding is additive

✓

The embedding \(K[x^{\pm }] \hookrightarrow K(\! (x)\! )\) preserves addition: for Laurent polynomials \(p\) and \(q\), the image of \(p + q\) equals the sum of the images.

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_add {K : Type u_1} [CommRing K] (p q : LaurentPolynomial K) :

laurentPolynomialToSeries (p + q) = laurentPolynomialToSeries p + laurentPolynomialToSeries q

Proof ▶

By extensionality on coefficients: both sides have the same coefficient at each \(n \in \mathbb {Z}\).

Lemma A.119 Laurent polynomial embedding preserves 1

✓

The embedding \(K[x^{\pm }] \hookrightarrow K(\! (x)\! )\) sends \(1\) to \(1\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_one {K : Type u_1} [CommRing K] :

laurentPolynomialToSeries 1 = 1

Proof ▶

By extensionality on coefficients.

Lemma A.120 Laurent polynomial embedding preserves coefficients

✓

For any Laurent polynomial \(p\) and any \(n \in \mathbb {Z}\), the \(n\)-th coefficient of the image equals \(p(n)\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.laurentPolynomialToSeries_coeff {K : Type u_1} [CommRing K] (p : LaurentPolynomial K) (n : ℤ) :

(laurentPolynomialToSeries p).coeff n = p n

Proof ▶

By definition of the embedding.

A.5.8 Helpers for Theorem 1.483

Lemma A.121 Existence of balanced ternary representation

✓

For any integer \(n\), there exists a balanced ternary representation of \(n\). The proof finds \(k\) large enough that \(|n| \le M_k\), then uses the \(k\)-bounded existence result (Lemma 1.485).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.balancedTernary_exists (n : ℤ) :

Nonempty (BalancedTernaryRep n)

Proof ▶

Find \(k\) with \(|n| \le M_k\) (using \(|n| \le M_{|n|}\)). Then \(n \in [-M_k, M_k]\), so by Lemma 1.485 there exists a \(k\)-bounded representation, which is converted to a finitely supported function.

Lemma A.122 Uniqueness of balanced ternary representation

✓

If two balanced ternary representations have the same value \(n\), then their digit functions are equal. This follows from Lemma 1.484 applied to the difference of the two digit sequences.

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.balancedTernary_unique (n : ℤ) (r1 r2 : BalancedTernaryRep n) :

r1.digits = r2.digits

Proof ▶

Apply the uniqueness result for balanced ternary digits to the two digit functions, using that both have values in \(\{ -1, 0, 1\} \) and the same weighted sum.

Lemma A.123 \(k\)-bounded values lie in the target interval

✓

For any \(k\)-bounded balanced ternary representation \(f \in \{ -1, 0, 1\} ^{k+1}\), the value \(\sum _{i=0}^{k} f(i) \cdot 3^i\) lies in the interval \([-M_k, M_k]\) where \(M_k = \sum _{i=0}^{k} 3^i\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedBTValue_mem_Icc (k : ℕ) (f : Fin (k + 1) → ℤ) (hf : f ∈ kBoundedBTReps k) :

kBoundedBTValue k f ∈ Icc_symm (maxBT k)

Proof ▶

Each digit \(f(i) \in \{ -1, 0, 1\} \) contributes at most \(\pm 3^i\) to the sum. Summing gives the bounds \(-\sum 3^i \le \text{value} \le \sum 3^i\).

Lemma A.124 Balanced ternary injectivity

The evaluation map \(f \mapsto \sum _{i=0}^{k} f(i) \cdot 3^i\) is injective on the set of \(k\)-bounded balanced ternary representations.

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.kBoundedBTValue_injective_on (k : ℕ) :

Set.InjOn (kBoundedBTValue k) ↑(kBoundedBTReps k)

Proof ▶

By strong induction on \(k\): the lowest digit is determined by the value modulo \(3\), and the remaining digits are determined by induction on the quotient.

Lemma A.125 Digit differences are bounded

✓

If \(a, b \in \{ -1, 0, 1\} \), then \(|a - b| \le 2\). If additionally \(a \ne b\), then \(|a - b| \ge 1\).

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.btDigits_diff_abs_ge_one {a b : ℤ} (ha : a ∈ btDigits) (hb : b ∈ btDigits) (hab : a ≠ b) :

|a - b| ≥ 1

docs source

theorem AlgebraicCombinatorics.FPS.Laurent.btDigits_diff_abs_le_two {a b : ℤ} (ha : a ∈ btDigits) (hb : b ∈ btDigits) :

|a - b| ≤ 2

Proof ▶

By case analysis on \(a\) and \(b\).

Lemma A.126 Equivalence of balanced ternary representation types

There is a type equivalence between the finitely-supported balanced ternary representation (using \(\mathbb {N} \to \mathbb {Z}\) with digits in \(\{ -1,0,1\} \) and finite support) and the inductive-style balanced ternary representation. The conversions are inverse to each other.

docs source

noncomputable def AlgebraicCombinatorics.FPS.Laurent.balancedTernary_equiv (n : ℤ) :

BalancedTernaryRep n ≃ BTRep n

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

Proof ▶

The forward direction maps each digit \(d\) to its balanced ternary digit, the inverse maps each balanced ternary digit to its integer value. Round-trip identities follow by checking both compositions are the identity.

19s: Darij Grinberg, Introduction to Modern Algebra (UMN Spring 2019 Math 4281 notes), 29 June 2019.
http://www.cip.ifi.lmu.de/~grinberg/t/19s/notes.pdf
19s-mt3s: Darij Grinberg, Math 4281: Introduction to Modern Algebra, Spring 2019: Midterm 3 with solutions.
https://www.cip.ifi.lmu.de/~grinberg/t/19s/mt3s.pdf
19fco: Darij Grinberg, Enumerative Combinatorics: class notes (Drexel Fall 2019 Math 222 notes), 11 September 2022.
http://www.cip.ifi.lmu.de/~grinberg/t/19fco/n/n.pdf
Ford21: Timothy J. Ford, Abstract Algebra, draft of a book, 14 August 2024.
https://tim4datfau.github.io/Timothy-Ford-at-FAU/preprints/Algebra_Book.pdf
Grinbe15: Darij Grinberg, Notes on the combinatorial fundamentals of algebra, 15 September 2022.
http://www.cip.ifi.lmu.de/~grinberg/primes2015/sols.pdf
Grinbe17: Darij Grinberg, Why the log and exp series are mutually inverse, 11 May 2018.
https://www.cip.ifi.lmu.de/~grinberg/t/17f/logexp.pdf
Laue15: Hartmut Laue, Determinants, version 17 May 2015,
http://www.math.uni-kiel.de/algebra/laue/homepagetexte/det.pdf
Strick13: Neil Strickland, MAS201 Linear Mathematics for Applications, lecture notes, 11 February 2020.
https://neilstrickland.github.io/linear_maths/notes/linear_maths.pdf
Zeilbe85: Doron Zeilberger, A combinatorial approach to matrix algebra, Discrete Mathematics 56 (1985), pp. 61–72.
20f: Darij Grinberg, Math 235: Mathematical Problem Solving, 22 March 2021.
http://www.cip.ifi.lmu.de/~grinberg/t/20f/mps.pdf
Benede25: Bruno Benedetti, Introduction to Abstract Algebra “Rings First”, lecture notes, 6 March 2025.
https://www.math.miami.edu/~bruno/algebra2.pdf
BluCos16: Ben Blum-Smith, Samuel Coskey, The Fundamental Theorem on Symmetric Polynomials: History’s First Whiff of Galois Theory, arXiv:1301.7116v5.
Bresso99: David M. Bressoud, Proofs and Confirmations: The Story of the Alternating Sign Matrix Conjecture, Cambridge University Press 1999.
See http://web.archive.org/web/20220531023303/https://www.macalester.edu/~bressoud/books/PnC/PnCcorrect.html
Dumas08: François Dumas, An introduction to noncommutative polynomial invariants, lecture notes (Cimpa-Unesco-Argentina “Homological methods and representations of non-commutative algebras”, Mar del Plata, Argentina March 6 - 17, 2006).
https://lmbp.uca.fr/~fdumas/fichiers/CIMPA.pdf
Goodma15: Frederick M. Goodman, Algebra: Abstract and Concrete, edition 2.6, 1 May 2015.
http://homepage.math.uiowa.edu/~goodman/algebrabook.dir/book.2.6.pdf .
Loehr11: Nicholas A. Loehr, Bijective Combinatorics, Chapman & Hall/CRC 2011.
Smith95: Larry Smith, Polynomial Invariants of Finite Groups, A K Peters 1995.
Bourba74: Nicolas Bourbaki, Algebra I: Chapters 1–3, Addison-Wesley 1974.
Zeilbe98: Doron Zeilberger, Dodgson’s Determinant-Evaluation Rule proved by Two-Timing Men and Women, The Electronic Journal of Combinatorics, vol. 4, issue 2 (1997) (The Wilf Festschrift).