Milnor K-groups $K^M_n(F)$ and symbols

Ambient data (variable binders). Throughout, $F$ is a field whose underlying type lives in the lowest universe (Type, i.e. a "small" type). Write $F^\times$ for its group of units (the nonzero elements under multiplication), and $A := \operatorname{Additive}(F^\times)$ for the same group written additively: the element of $A$ corresponding to $u \in F^\times$ is denoted $[u]$, and $[uv] = [u] + [v]$, $[1] = 0$, $k\cdot[u] = [u^k]$ for $k \in \mathbb{Z}$. $A$ is regarded as a $\mathbb{Z}$-module via this abelian-group structure. For $n \in \mathbb{N}$, $A^{\otimes n} := \bigotimes_{\mathbb{Z}}^{\,n} A$ denotes the $n$-fold tensor power of $A$ over $\mathbb{Z}$, formally the tensor product over $\mathbb{Z}$ of the family $(A)_{l \in \{0,\dots,n-1\}}$ indexed by $\operatorname{Fin} n = \{0, 1, \dots, n-1\}$. For a tuple $a = (a_0,\dots,a_{n-1}) \in (F^\times)^n$, write $[a_0]\otimes\cdots\otimes[a_{n-1}]$ for the corresponding pure tensor. No other hypotheses on $F$ (characteristic, finiteness, etc.) are imposed.

steinberg F n (definition). For each $n \in \mathbb{N}$, this is the $\mathbb{Z}$-submodule (subgroup) $\mathrm{St}_n(F) \subseteq A^{\otimes n}$ generated by the set

That is, the generators are exactly the pure tensors of units in which some two consecutive entries $a_i, a_{i+1}$ (adjacent positions, in that order) sum to $1$ in $F$ (the sum is taken in the field $F$, not in the group $A$). Pairs of non-adjacent positions are not included directly among the generators. Since the $a_l$ are units, such a pair requires $a_i \neq 0$, $a_{i+1} = 1 - a_i \neq 0$, i.e. $a_i \notin \{0, 1\}$. The index condition "$j = i+1$" is read on natural numbers with both $i, j < n$, so no wrap-around from position $n-1$ to position $0$ occurs. Degenerate cases: for $n = 0$ and $n = 1$ there is no pair of positions $i, i+1$ both $< n$, so $S_0 = S_1 = \varnothing$ and $\mathrm{St}_0(F) = \mathrm{St}_1(F) = 0$. For $n \ge 2$ the set $S_n$ is nonempty exactly when some $u \in F^\times$ has $1-u \in F^\times$ (i.e. $|F| > 2$); for $F = \mathbb{F}_2$, $S_n = \varnothing$ (though then $A = 0$ and $A^{\otimes n} = 0$ for $n \ge 1$ anyway).

MilnorK F n (abbreviation). For each $n \in \mathbb{N}$, this is the quotient $\mathbb{Z}$-module (abelian group)

with its induced abelian-group / $\mathbb{Z}$-module structure. It is a plain family of abelian groups indexed by $n$; no multiplication or graded-ring structure between different $n$ is defined in this file. Degenerate cases: since $\mathrm{St}_0 = \mathrm{St}_1 = 0$, $K_0(F)$ is the empty tensor power $A^{\otimes 0}$, which (by Mathlib's conventions) is canonically $\mathbb{Z}$, and $K_1(F) = A^{\otimes 1}$, which is canonically $A \cong F^\times$ (written additively), with no relations imposed in either case.

symbol (definition). Implicit arguments: the field $F$ (as above) and $n \in \mathbb{N}$; explicit argument: a tuple $a = (a_0,\dots,a_{n-1}) \in (F^\times)^n$. The value is

where $\pi : A^{\otimes n} \to K_n(F)$ is the canonical quotient map ($\mathbb{Z}$-linear, surjective). It is marked noncomputable, which has no mathematical content. For $n = 0$ the only tuple is the empty one and $\{\,\}$ is the image of the empty pure tensor (corresponding to $1 \in \mathbb{Z}$). By construction and multilinearity of the pure tensor, $\{a_0,\dots,a_{n-1}\} = 0$ whenever $a_i + a_{i+1} = 1$ for some $i$ with $i+1 < n$, and $\{\dots, uv, \dots\} = \{\dots, u, \dots\} + \{\dots, v, \dots\}$ in each slot; the file itself states no lemmas about symbol.

Lemmas. The file contains no theorems or lemmas; it consists only of the two variable declarations for $F$, the definitions steinberg and symbol, and the abbreviation MilnorK, all inside the namespace MilnorConjecture. The only notation opened is the tensor-product notation.