MilnorKTheory.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

39 declarations, 0 contain sorry, 0 declared as axioms

Milnor K-theory of a field modulo `ℓ`, symbols and symbol length

Milnor [Milnor1970] defined the graded ring $K^M_*(F)$ of a field $F$ as the quotient of the tensor algebra of the abelian group $F^\times$, written additively, by the two-sided ideal generated by the elements $\{a\} \otimes \{b\}$ with $a + b = 1$ (the Steinberg relations). This file defines:

MilnorK F ℓ: the ring $K^M_*(F)/\ell$, the quotient of TensorAlgebra ℤ (Additive Fˣ) by the Steinberg relations and the relation ℓ = 0. For ℓ = 0 it is $K^M_*(F)$ itself;
MilnorK.of ℓ a: the class $\{a\}$ of a unit a;
MilnorK.symbol ℓ a: the symbol $\{a_1, \dots, a_n\} = \{a_1\} \cdots \{a_n\}$ of an n-tuple of units;
MilnorK.grade F ℓ n: the degree-n part $K^M_n(F)/\ell$, the additive subgroup generated by the symbols of degree n;
MilnorK.symbolLengthBounds F ℓ n: the set of m such that every element of $K^M_n(F)/\ell$ is a sum of at most m symbols. Its least element, when it exists, is the symbol length of $K^M_n(F)/\ell$ [Krashen2024, §2.1.3.4].
MilnorK.augmentation F ℓ: the augmentation $K^M_*(F)/\ell \to \mathbb{Z}/\ell$, which shows that MilnorK F ℓ is nontrivial for ℓ ≠ 1 (MilnorK.nontrivial);
MilnorK.toDualNumber F ℓ φ: the map to the dual numbers $(\mathbb{Z}/\ell)[\varepsilon]$ attached to a homomorphism $\varphi \colon F^\times \to \mathbb{Z}/\ell$. It detects degree one, so the Steinberg relations do not collapse $K^M_1(F)/\ell$ (MilnorK.of_ne_zero, MilnorK.grade_one_ne_bot). It says nothing about the degrees ≥ 2, where the symbol length problem lives.

In degree 0 the symbols are all equal to the empty product 1, so $K^M_0(F)/\ell = \mathbb{Z}/\ell$ has symbol length ℓ - 1 for ℓ ≥ 1 (MilnorK.isLeast_symbolLengthBounds_zero). In degree 1 every class is a single symbol, so the symbol length of $K^M_1(F)/\ell$ is at most 1 (MilnorK.one_mem_symbolLengthBounds_one), with equality as soon as the group is nonzero (MilnorK.isLeast_symbolLengthBounds_one).

The defining ideal is homogeneous, so the degree-n part of the quotient is the image of the degree-n part of the tensor algebra, which is spanned by the symbols. No numeric symbol length is defined, so that no convention is needed when symbolLengthBounds F ℓ n is empty.

References

[Milnor1970] J. Milnor, Algebraic K-theory and quadratic forms, Invent. Math. 9 (1970), 318–344, doi:10.1007/BF01425486.
[Krashen2024] D. Krashen, PCMI Summer School (not quite) notes, notes for the minicourse Field arithmetic and the complexity of algebraic objects, PCMI Graduate Summer School on Motivic Homotopy Theory, 2024, draft of 24 July 2024, pdf.

Imports (5)

Imported by 1 file

FormalConjecturesForMathlib.lean

inductive MilnorK.Rel The relations defining K^M_*(F)/ℓ as a quotient of the tensor algebra of Fˣ: the Steinberg relation {a}{b} = 0 when a + b = 1, and the relation ℓ = 0 line 80 source
Source documentation
The relations defining K^M_*(F)/ℓ as a quotient of the tensor algebra of Fˣ: the Steinberg relation {a}{b} = 0 when a + b = 1, and the relation ℓ = 0.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, TensorAlgebra, Int, Additive, Units
12 instances, coercions and auxiliary constants left out.
```
inductive Rel (ℓ : ℕ) : TensorAlgebra ℤ (Additive Fˣ) → TensorAlgebra ℤ (Additive Fˣ) → Prop
  | steinberg (a b : Fˣ) (h : (a : F) + (b : F) = 1) :
      Rel ℓ (ι ℤ (Additive.ofMul a) * ι ℤ (Additive.ofMul b)) 0
  | natCast : Rel ℓ (ℓ : TensorAlgebra ℤ (Additive Fˣ)) 0

end MilnorK

/-- The Milnor K-ring `K^M_*(F)/ℓ` of the field `F` with coefficients in `ℤ/ℓ`. For `ℓ = 0`
this is the Milnor K-ring `K^M_*(F)`. -/
```
Mentions: MilnorK, MilnorK.of
abbrev MilnorK The Milnor K-ring K^M_*(F)/ℓ of the field F with coefficients in ℤ/ℓ line 89 source
Source documentation
The Milnor K-ring K^M_*(F)/ℓ of the field F with coefficients in ℤ/ℓ. For ℓ = 0 this is the Milnor K-ring K^M_*(F).

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat
Proof uses: RingQuot, TensorAlgebra, Int, Additive, Units, MilnorK.Rel
13 instances, coercions and auxiliary constants left out.
```
abbrev MilnorK (ℓ : ℕ) := RingQuot (MilnorK.Rel F ℓ)
…
```
Mentions: MilnorK.Rel
def MilnorK.of The class {a} of a unit a in K^M_1(F)/ℓ line 96 source
Source documentation
The class {a} of a unit a in K^M_1(F)/ℓ.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, MilnorK
Proof uses: RingHom, TensorAlgebra, Int, Additive, RingQuot, MilnorK.Rel, RingQuot.mkRingHom, LinearMap, RingHom.id, TensorAlgebra.ι, Equiv, Additive.ofMul
30 instances, coercions and auxiliary constants left out.
```
def of (a : Fˣ) : MilnorK F ℓ := RingQuot.mkRingHom (Rel F ℓ) (ι ℤ (Additive.ofMul a))
…
```
Mentions: MilnorK, MilnorK.Rel
theorem MilnorK.of_one line 99 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Eq, MilnorK, MilnorK.of, OfNat.ofNat, Units, TensorAlgebra, Int, Additive, MilnorK.Rel
Proof uses: of_eq_true, Eq.trans, RingQuot, True, congrFun', congrArg, RingHom, RingQuot.mkRingHom, LinearMap, RingHom.id, TensorAlgebra.ι, Equiv, Additive.ofMul, map_zero, eq_self
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.of_mul line 103 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, MilnorK, MilnorK.of, HMul.hMul, HAdd.hAdd, TensorAlgebra, Int, Additive, MilnorK.Rel
Proof uses: of_eq_true, RingHom, RingQuot, RingQuot.mkRingHom, LinearMap, RingHom.id, TensorAlgebra.ι, Equiv, Additive.ofMul, Eq.trans, True, congrFun', congrArg, map_add, eq_self
60 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.of_inv line 107 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, MilnorK, MilnorK.of, Inv.inv, Neg.neg, TensorAlgebra, Int, Additive, MilnorK.Rel
Proof uses: of_eq_true, RingHom, RingQuot, RingQuot.mkRingHom, LinearMap, RingHom.id, TensorAlgebra.ι, Equiv, Additive.ofMul, Eq.trans, True, congrFun', congrArg, map_neg, eq_self
63 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.of_pow line 111 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, MilnorK, MilnorK.of, HPow.hPow, HSMul.hSMul, TensorAlgebra, Int, Additive, MilnorK.Rel
Proof uses: Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congr, congrArg, pow_zero, MilnorK.of_one, zero_nsmul, eq_self, Eq.mpr, HAdd.hAdd, HMul.hMul, id, pow_succ, MilnorK.of_mul, succ_nsmul, Eq.refl
68 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def MilnorK.ofHom The class map {·} : Fˣ → K^M_1(F)/ℓ as an additive homomorphism line 117 source
Source documentation
The class map {·} : Fˣ → K^M_1(F)/ℓ as an additive homomorphism.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, AddMonoidHom, Additive, Units, MilnorK, TensorAlgebra, Int, MilnorK.Rel
Proof uses: AddMonoidHom.mk, ZeroHom.mk, MilnorK.of, Equiv, Additive.toMul
50 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def ofHom : Additive Fˣ →+ MilnorK F ℓ where
…
```
Mentions: MilnorK
theorem MilnorK.ofHom_apply line 123 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Additive, Units, Eq, MilnorK, AddMonoidHom, TensorAlgebra, Int, MilnorK.Rel, MilnorK.ofHom, MilnorK.of, Equiv, Additive.toMul
Proof uses: rfl
50 instances, coercions and auxiliary constants left out.
theorem MilnorK.of_mul_of_eq_zero The Steinberg relation {a}{b} = 0 when a + b = 1 line 126 source
Source documentation
The Steinberg relation {a}{b} = 0 when a + b = 1.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, HAdd.hAdd, OfNat.ofNat, MilnorK, HMul.hMul, TensorAlgebra, Int, Additive, MilnorK.Rel, MilnorK.of
Proof uses: Eq.mpr, RingHom, RingQuot, RingQuot.mkRingHom, LinearMap, RingHom.id, TensorAlgebra.ι, Equiv, Additive.ofMul, id, congrArg, MilnorK.of.eq_1, Eq.symm, map_mul, RingQuot.mkRingHom_rel, MilnorK.Rel.steinberg, map_zero, Eq.refl
81 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem of_mul_of_eq_zero (a b : Fˣ) (h : (a : F) + (b : F) = 1) : of ℓ a * of ℓ b = 0 := by
…
```
Mentions: MilnorK.of
theorem MilnorK.natCast_eq_zero The relation ℓ = 0 in K^M_*(F)/ℓ line 131 source
Source documentation
The relation ℓ = 0 in K^M_*(F)/ℓ.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Eq, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, OfNat.ofNat
Proof uses: Eq.mpr, RingHom, RingQuot, RingQuot.mkRingHom, id, congrArg, Eq.symm, map_natCast, RingQuot.mkRingHom_rel, MilnorK.Rel.natCast, map_zero, Eq.refl
51 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem natCast_eq_zero : (ℓ : MilnorK F ℓ) = 0 := by
…
```
Mentions: MilnorK
def MilnorK.symbol The symbol {a 0, …, a (n - 1)} = {a 0} ⋯ {a (n - 1)} of an n-tuple of units line 136 source
Source documentation
The symbol {a 0, …, a (n - 1)} = {a 0} ⋯ {a (n - 1)} of an n-tuple of units.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Fin, Units, MilnorK
Proof uses: List.prod, TensorAlgebra, Int, Additive, MilnorK.Rel, List.ofFn, MilnorK.of
19 instances, coercions and auxiliary constants left out.
```
def symbol {n : ℕ} (a : Fin n → Fˣ) : MilnorK F ℓ := (List.ofFn fun i ↦ of ℓ (a i)).prod
…
```
Mentions: MilnorK, MilnorK.of
theorem MilnorK.symbol_zero line 139 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Fin, OfNat.ofNat, Units, Eq, MilnorK, MilnorK.symbol, TensorAlgebra, Int, Additive, MilnorK.Rel
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, List, List.ofFn, MilnorK.of, List.nil, List.prod, List.ofFn_zero, eq_self
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.symbol_succ line 142 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Fin, HAdd.hAdd, OfNat.ofNat, Units, Eq, MilnorK, MilnorK.symbol, HMul.hMul, TensorAlgebra, Int, Additive, MilnorK.Rel, MilnorK.of, Fin.succ
Proof uses: of_eq_true, List.prod, List.ofFn, Eq.trans, True, congrFun', congrArg, List, List.cons, List.ofFn_succ, eq_self
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.symbol_one line 147 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Fin, OfNat.ofNat, Units, Eq, MilnorK, MilnorK.symbol, MilnorK.of
Proof uses: of_eq_true, Eq.trans, HAdd.hAdd, True, congrFun', congrArg, HMul.hMul, TensorAlgebra, Int, Additive, MilnorK.Rel, Fin.succ, MilnorK.symbol_succ, MilnorK.symbol_zero, mul_one, eq_self
33 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.symbol_pair line 150 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, MilnorK, MilnorK.symbol, Nat.succ, OfNat.ofNat, Matrix.vecCons, Matrix.vecEmpty, HMul.hMul, TensorAlgebra, Int, Additive, MilnorK.Rel, MilnorK.of
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, Fin, Fin.succ, MilnorK.symbol_succ, funext, Matrix.cons_val_succ, Matrix.cons_val_fin_one, MilnorK.symbol_one, eq_self
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.symbol_pair_eq_zero The Steinberg relation {a, b} = 0 when a + b = 1 line 154 source
Source documentation
The Steinberg relation {a, b} = 0 when a + b = 1.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, HAdd.hAdd, OfNat.ofNat, MilnorK, MilnorK.symbol, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, TensorAlgebra, Int, Additive, MilnorK.Rel
Proof uses: Eq.mpr, HMul.hMul, MilnorK.of, id, congrArg, MilnorK.symbol_pair, MilnorK.of_mul_of_eq_zero, Eq.refl
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_pair_eq_zero (a b : Fˣ) (h : (a : F) + (b : F) = 1) : symbol ℓ ![a, b] = 0 := by
…
```
Mentions: MilnorK.symbol
def MilnorK.grade The degree-n part K^M_n(F)/ℓ of K^M_*(F)/ℓ: the additive subgroup generated by the symbols of degree n line 161 source
Source documentation
The degree-n part K^M_n(F)/ℓ of K^M_*(F)/ℓ: the additive subgroup generated by the symbols of degree n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel
Proof uses: AddSubgroup.closure, Set.range, Fin, MilnorK.symbol
34 instances, coercions and auxiliary constants left out.
```
def grade (n : ℕ) : AddSubgroup (MilnorK F ℓ) :=
…
```
Mentions: MilnorK
theorem MilnorK.symbol_mem_grade line 164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Fin, Units, Membership.mem, MilnorK, AddSubgroup, TensorAlgebra, Int, Additive, MilnorK.Rel, MilnorK.grade, MilnorK.symbol
Proof uses: AddSubgroup.subset_closure, Set.range, Exists.intro, Eq, rfl
36 instances, coercions and auxiliary constants left out.
def MilnorK.symbolLengthBounds The set of m such that every element of K^M_n(F)/ℓ is a sum of at most m symbols line 169 source
Source documentation
The set of m such that every element of K^M_n(F)/ℓ is a sum of at most m symbols. Its least element, when it exists, is the symbol length of K^M_n(F)/ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Set
Proof uses: Set.ofPred, MilnorK, Membership.mem, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Exists, And, LE.le, Fin, Eq, Finset.sum, Finset.univ, MilnorK.symbol
23 instances, coercions and auxiliary constants left out.
```
def symbolLengthBounds (n : ℕ) : Set ℕ :=
…
```
theorem MilnorK.mem_symbolLengthBounds_of_le line 172 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Membership.mem, Set, MilnorK.symbolLengthBounds, LE.le
Proof uses: MilnorK, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Exists, And, Fin, Eq, Finset.sum, Finset.univ, MilnorK.symbol, Exists.intro, And.intro, LE.le.trans
28 instances, coercions and auxiliary constants left out.
theorem MilnorK.zero_mem_symbolLengthBounds_iff line 176 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Iff, Membership.mem, Set, MilnorK.symbolLengthBounds, OfNat.ofNat, Eq, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Bot.bot
Proof uses: Iff.intro, Eq.mpr, LE.le, id, congrArg, propext, eq_bot_iff, And, Exists, Fin, Finset.sum, Finset.univ, MilnorK.symbol, of_eq_true, Eq.trans, True, Finset.sum_congr, EmptyCollection.emptyCollection, Finset, Finset.univ_eq_empty and 12 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.grade_eq_bot_of_forall_exists_pow_eq If every unit of F is an ℓ-th power, then K^M_n(F)/ℓ = 0 for n ≥ 1 line 190 source
Source documentation
If every unit of F is an ℓ-th power, then K^M_n(F)/ℓ = 0 for n ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Exists, Eq, HPow.hPow, Ne, OfNat.ofNat, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, MilnorK.Rel, MilnorK.grade, Bot.bot
Proof uses: Eq.mpr, LE.le, id, congrArg, propext, eq_bot_iff, AddSubgroup.closure, Set.range, Fin, MilnorK.symbol, MilnorK.grade.eq_1, Set, AddSubgroup.closure_le, Membership.mem, HAdd.hAdd, Nat.exists_eq_add_one_of_ne_zero, SetLike.mem_coe, AddSubgroup.mem_bot, HMul.hMul, MilnorK.of and 9 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem grade_eq_bot_of_forall_exists_pow_eq (h : ∀ a : Fˣ, ∃ b : Fˣ, b ^ ℓ = a) {n : ℕ}
    (hn : n ≠ 0) : grade F ℓ n = ⊥ := by
…
```
Mentions: MilnorK.grade
def MilnorK.augmentation The augmentation K^M_*(F)/ℓ → ℤ/ℓ, which sends every class {a} to 0 line 200 source
Source documentation
The augmentation K^M_*(F)/ℓ → ℤ/ℓ, which sends every class {a} to 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, RingHom, MilnorK, ZMod, TensorAlgebra, Int, Additive, Units, MilnorK.Rel
Proof uses: Equiv, Subtype, Eq, RingQuot, RingQuot.lift, Subtype.mk, AlgHom.toRingHom, LinearMap, RingHom.id, AlgHom, TensorAlgebra.lift, OfNat.ofNat
52 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def augmentation : MilnorK F ℓ →+* ZMod ℓ :=
…
```
Mentions: MilnorK
theorem MilnorK.augmentation_of line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Units, Eq, ZMod, RingHom, MilnorK, TensorAlgebra, Int, Additive, MilnorK.Rel, MilnorK.augmentation, MilnorK.of, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, RingQuot, Equiv, Subtype, RingQuot.lift, Subtype.mk, AlgHom, LinearMap, RingHom.id, TensorAlgebra.lift, AlgHom.toRingHom, id, Eq.refl, RingQuot.mkRingHom, TensorAlgebra.ι, Additive.ofMul and 3 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.nontrivial K^M_*(F)/ℓ is nontrivial for ℓ ≠ 1, since the augmentation maps it onto ℤ/ℓ line 212 source
Source documentation
K^M_*(F)/ℓ is nontrivial for ℓ ≠ 1, since the augmentation maps it onto ℤ/ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Ne, OfNat.ofNat, Nontrivial, MilnorK
Proof uses: ZMod, Nat.casesAuxOn, HAdd.hAdd, absurd, Eq, rfl, Fact, LT.lt, Fact.mk, Decidable.byContradiction, Not, inferInstance, RingHom.domain_nontrivial, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.augmentation
27 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem nontrivial (hℓ : ℓ ≠ 1) : Nontrivial (MilnorK F ℓ) := by
…
```
Mentions: MilnorK
theorem MilnorK.one_mem_grade_zero The empty symbol is 1, so 1 ∈ K^M_0(F)/ℓ line 222 source
Source documentation
The empty symbol is 1, so 1 ∈ K^M_0(F)/ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Membership.mem, MilnorK, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, OfNat.ofNat
Proof uses: Eq.mp, MilnorK.symbol, Fin.elim0, congrArg, MilnorK.symbol_zero, MilnorK.symbol_mem_grade
46 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem one_mem_grade_zero : (1 : MilnorK F ℓ) ∈ grade F ℓ 0 := by
…
```
Mentions: MilnorK, MilnorK.grade
theorem MilnorK.mem_grade_zero_iff K^M_0(F)/ℓ = ℤ/ℓ is generated by the empty symbol 1 line 226 source
Source documentation
K^M_0(F)/ℓ = ℤ/ℓ is generated by the empty symbol 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, MilnorK, Iff, Membership.mem, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, OfNat.ofNat, Exists, Eq
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, AddSubgroup.closure, Singleton.singleton, Set, Set.range, Fin, MilnorK.symbol, Inhabited.default, Set.range_unique, MilnorK.symbol_zero, funext, HMul.hMul, zsmul_eq_mul, mul_one, iff_self
67 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem mem_grade_zero_iff {x : MilnorK F ℓ} : x ∈ grade F ℓ 0 ↔ ∃ z : ℤ, (z : MilnorK F ℓ) = x := by
…
```
Mentions: MilnorK, MilnorK.grade
theorem MilnorK.sub_one_le_of_mem_symbolLengthBounds_zero Documented declaration: sub_one_le_of_mem_symbolLengthBounds_zero line 231 source
Source documentation
Every bound on the symbol length of K^M_0(F)/ℓ = ℤ/ℓ is at least ℓ - 1: the augmentation sends a sum of j empty symbols to j, so the class of ℓ - 1 needs at least ℓ - 1 symbols.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, LT.lt, OfNat.ofNat, Membership.mem, Set, MilnorK.symbolLengthBounds, LE.le, HSub.hSub
Proof uses: MilnorK, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Eq.mp, HSMul.hSMul, congrArg, Eq.trans, HMul.hMul, nsmul_eq_mul, mul_one, AddSubgroup.nsmul_mem, MilnorK.one_mem_grade_zero, And, Exists, Fin and 21 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem sub_one_le_of_mem_symbolLengthBounds_zero {k : ℕ} (hℓ : 0 < ℓ)
    (hk : k ∈ symbolLengthBounds F ℓ 0) : ℓ - 1 ≤ k := by
…
```
Mentions: MilnorK.symbolLengthBounds
theorem MilnorK.sub_one_mem_symbolLengthBounds_zero Every element of K^M_0(F)/ℓ = ℤ/ℓ is a sum of at most ℓ - 1 empty symbols line 244 source
Source documentation
Every element of K^M_0(F)/ℓ = ℤ/ℓ is a sum of at most ℓ - 1 empty symbols.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, LT.lt, OfNat.ofNat, Membership.mem, Set, MilnorK.symbolLengthBounds, HSub.hSub
Proof uses: MilnorK, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Eq, Exists, And, LE.le, Fin, Finset.sum, Finset.univ, MilnorK.symbol, Iff.mp, MilnorK.mem_grade_zero_iff, Ne, Exists.intro and 37 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem sub_one_mem_symbolLengthBounds_zero (hℓ : 0 < ℓ) : ℓ - 1 ∈ symbolLengthBounds F ℓ 0 := by
…
```
Mentions: MilnorK.symbolLengthBounds
theorem MilnorK.isLeast_symbolLengthBounds_zero For ℓ ≥ 1, the symbol length of K^M_0(F)/ℓ = ℤ/ℓ is ℓ - 1 line 259 source
Source documentation
For ℓ ≥ 1, the symbol length of K^M_0(F)/ℓ = ℤ/ℓ is ℓ - 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, LT.lt, OfNat.ofNat, IsLeast, MilnorK.symbolLengthBounds, HSub.hSub
Proof uses: And.intro, Membership.mem, Set, lowerBounds, MilnorK.sub_one_mem_symbolLengthBounds_zero, MilnorK.sub_one_le_of_mem_symbolLengthBounds_zero
11 instances, coercions and auxiliary constants left out.
```
theorem isLeast_symbolLengthBounds_zero (hℓ : 0 < ℓ) :
    IsLeast (symbolLengthBounds F ℓ 0) (ℓ - 1) :=
…
```
Mentions: MilnorK.symbolLengthBounds
def MilnorK.toDualNumber Documented declaration: toDualNumber line 275 source
Source documentation
The map to the dual numbers (ℤ/ℓ)[ε] attached to a homomorphism φ : Fˣ → ℤ/ℓ: it sends {a} to φ(a) ε and kills every product of two classes of degree one, so in particular it kills the Steinberg relations.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, AddMonoidHom, Additive, Units, ZMod, RingHom, MilnorK, DualNumber, TensorAlgebra, Int, MilnorK.Rel
Proof uses: Equiv, Subtype, Eq, RingQuot, RingQuot.lift, Subtype.mk, AlgHom.toRingHom, TrivSqZeroExt, LinearMap, RingHom.id, AlgHom, TensorAlgebra.lift, LinearMap.comp, TrivSqZeroExt.inrHom, AddMonoidHom.toIntLinearMap
83 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
noncomputable def toDualNumber (φ : Additive Fˣ →+ ZMod ℓ) :
    MilnorK F ℓ →+* DualNumber (ZMod ℓ) :=
…
```
Mentions: MilnorK
theorem MilnorK.toDualNumber_of line 288 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, AddMonoidHom, Additive, Units, ZMod, Eq, DualNumber, RingHom, MilnorK, TensorAlgebra, Int, MilnorK.Rel, MilnorK.toDualNumber, MilnorK.of, TrivSqZeroExt.inr, Equiv, Additive.ofMul
Proof uses: of_eq_true, Eq.trans, HSMul.hSMul, DualNumber.eps, True, congr, TrivSqZeroExt, congrArg, RingQuot, Subtype, RingQuot.lift, Subtype.mk, AlgHom, LinearMap, RingHom.id, TensorAlgebra.lift, LinearMap.comp, TrivSqZeroExt.inrHom, AddMonoidHom.toIntLinearMap, AlgHom.toRingHom and 9 more
117 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem MilnorK.of_ne_zero Degree one does not collapse: if a homomorphism φ : Fˣ → ℤ/ℓ is nonzero on a, then the class {a} is nonzero in K^M_1(F)/ℓ line 294 source
Source documentation
Degree one does not collapse: if a homomorphism φ : Fˣ → ℤ/ℓ is nonzero on a, then the class {a} is nonzero in K^M_1(F)/ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, AddMonoidHom, Additive, Units, ZMod, Ne, Equiv, Additive.ofMul, OfNat.ofNat, MilnorK, MilnorK.of, TensorAlgebra, Int, MilnorK.Rel
Proof uses: Eq, Eq.mp, TrivSqZeroExt.snd, RingHom, DualNumber, MilnorK.toDualNumber, congr, congrArg, Eq.trans, HSMul.hSMul, DualNumber.eps, TrivSqZeroExt.inr, MilnorK.toDualNumber_of, DualNumber.inr_eq_smul_eps, mul_one, map_zero
85 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem of_ne_zero (φ : Additive Fˣ →+ ZMod ℓ) (a : Fˣ)
    (hφ : φ (Additive.ofMul a) ≠ 0) : of ℓ a ≠ 0 :=
…
```
Mentions: MilnorK.of
theorem MilnorK.grade_one_ne_bot K^M_1(F)/ℓ ≠ 0 whenever some homomorphism φ : Fˣ → ℤ/ℓ is nonzero line 299 source
Source documentation
K^M_1(F)/ℓ ≠ 0 whenever some homomorphism φ : Fˣ → ℤ/ℓ is nonzero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, AddMonoidHom, Additive, Units, ZMod, Ne, Equiv, Additive.ofMul, OfNat.ofNat, AddSubgroup, MilnorK, TensorAlgebra, Int, MilnorK.Rel, MilnorK.grade, Bot.bot
Proof uses: Eq, MilnorK.of_ne_zero, Membership.mem, MilnorK.symbol, Fin, MilnorK.symbol_mem_grade, Eq.mp, MilnorK.of, congrFun', congrArg, MilnorK.symbol_one, propext, AddSubgroup.mem_bot
78 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem grade_one_ne_bot (φ : Additive Fˣ →+ ZMod ℓ) (a : Fˣ)
    (hφ : φ (Additive.ofMul a) ≠ 0) : grade F ℓ 1 ≠ ⊥ := by
…
```
Mentions: MilnorK.grade
theorem MilnorK.grade_one K^M_1(F)/ℓ is the image of Fˣ, since sums and negatives of degree-one symbols are again degree-one symbols line 309 source
Source documentation
K^M_1(F)/ℓ is the image of Fˣ, since sums and negatives of degree-one symbols are again degree-one symbols.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Eq, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, OfNat.ofNat, AddMonoidHom.range, MilnorK.ofHom
Proof uses: le_antisymm, Eq.mpr, LE.le, AddSubgroup.closure, Set.range, Fin, MilnorK.symbol, id, congrArg, MilnorK.grade.eq_1, Set, propext, AddSubgroup.closure_le, Membership.mem, Exists.intro, AddMonoidHom, Equiv, Additive.ofMul, of_eq_true, MilnorK.of and 7 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem grade_one : grade F ℓ 1 = (ofHom (F := F) ℓ).range := by
…
```
Mentions: MilnorK.grade, MilnorK.ofHom
theorem MilnorK.one_mem_symbolLengthBounds_one Every class in K^M_1(F)/ℓ is a single symbol line 318 source
Source documentation
Every class in K^M_1(F)/ℓ is a single symbol.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Membership.mem, Set, MilnorK.symbolLengthBounds, OfNat.ofNat
Proof uses: MilnorK, AddSubgroup, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Eq, AddMonoidHom, MilnorK.ofHom, AddMonoidHom.range, Exists, And, LE.le, Fin, Finset.sum, Finset.univ, MilnorK.symbol, Eq.le and 23 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem one_mem_symbolLengthBounds_one : 1 ∈ symbolLengthBounds F ℓ 1 := by
…
```
Mentions: MilnorK.symbolLengthBounds
theorem MilnorK.zero_notMem_symbolLengthBounds_one 0 is not a bound for the symbol length in degree 1 when K^M_1(F)/ℓ ≠ 0 line 324 source
Source documentation
0 is not a bound for the symbol length in degree 1 when K^M_1(F)/ℓ ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Ne, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, OfNat.ofNat, Bot.bot, Not, Membership.mem, Set, MilnorK.symbolLengthBounds
Proof uses: Iff.mp, Eq, MilnorK.zero_mem_symbolLengthBounds_iff
40 instances, coercions and auxiliary constants left out.
```
theorem zero_notMem_symbolLengthBounds_one (h : grade F ℓ 1 ≠ ⊥) :
    0 ∉ symbolLengthBounds F ℓ 1 :=
…
```
Mentions: MilnorK.grade, MilnorK.symbolLengthBounds
theorem MilnorK.isLeast_symbolLengthBounds_one The symbol length of K^M_1(F)/ℓ is 1 as soon as the group is nonzero line 330 source
Source documentation
The symbol length of K^M_1(F)/ℓ is 1 as soon as the group is nonzero. Use MilnorK.grade_one_ne_bot to get the hypothesis from a homomorphism Fˣ → ℤ/ℓ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Nat, Ne, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, OfNat.ofNat, Bot.bot, IsLeast, MilnorK.symbolLengthBounds
Proof uses: And.intro, Membership.mem, Set, lowerBounds, MilnorK.one_mem_symbolLengthBounds_one, Iff.mpr, LE.le, Nat.one_le_iff_ne_zero, Eq, MilnorK.zero_notMem_symbolLengthBounds_one, Eq.rec
41 instances, coercions and auxiliary constants left out.
```
theorem isLeast_symbolLengthBounds_one (h : grade F ℓ 1 ≠ ⊥) :
    IsLeast (symbolLengthBounds F ℓ 1) 1 :=
…
```
Mentions: MilnorK.grade, MilnorK.symbolLengthBounds

FormalConjecturesForMathlib/FieldTheory/MilnorKTheory.lean

Milnor K-theory of a field modulo ℓ, symbols and symbol length

References

`FormalConjecturesForMathlib/FieldTheory/MilnorKTheory.lean`

Milnor K-theory of a field modulo `ℓ`, symbols and symbol length