From d68bdbf3c7a41a78d8c1e70e5fd5ca4098c7265e Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 07:11:32 -0600
Subject: [PATCH 01/12] there goes

---
 .../SimplestExtension/AddMonoidAlgebra.lean   | 185 ++++++++++++++++++
 1 file changed, 185 insertions(+)
 create mode 100644 CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean

diff --git a/CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean b/CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean
new file mode 100644
index 00000000..371b409c
--- /dev/null
+++ b/CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean
@@ -0,0 +1,185 @@
+module
+
+public import CombinatorialGames.Nimber.SimplestExtension.Basic
+public import Mathlib.Algebra.MonoidAlgebra.Defs
+public import Mathlib.LinearAlgebra.Basis.Basic
+public import Mathlib.SetTheory.Ordinal.CantorNormalForm
+
+public noncomputable section
+
+open Ordinal
+
+/-! ### For Mathlib -/
+
+namespace Ordinal.CNF
+
+@[simp]
+theorem CNF_one (b : Ordinal) : CNF b 1 = [(0, 1)] := by
+  obtain hb | hb := le_or_gt b 1
+  · exact CNF.of_le_one hb one_ne_zero
+  · exact CNF.of_lt one_ne_zero hb
+
+theorem coeff_lt {b : Ordinal} (hb : 1 < b) (o e : Ordinal) : coeff b o e < b := by
+  by_cases he : e ∈ (CNF b o).map Prod.fst
+  · rw [List.mem_map, Prod.exists] at he
+    obtain ⟨c, _, hc, rfl⟩ := he
+    rw [coeff_of_mem_CNF hc]
+    exact snd_lt hb hc
+  · rw [coeff_of_notMem_CNF he]
+    exact hb.pos
+
+@[simp]
+theorem coeff_one (b : Ordinal) : coeff b 1 = Finsupp.single 0 1 := by
+  ext e
+  obtain rfl | he := eq_or_ne e 0
+  · rw [Finsupp.single_eq_same]
+    apply coeff_of_mem_CNF
+    simp
+  · rw [coeff_of_notMem_CNF]
+    · simp [he]
+    · simpa
+
+end Ordinal.CNF
+
+namespace Finsupp
+variable {M N α : Type*} [AddZeroClass M] [AddZeroClass N]
+
+theorem mapRange_single_add {f : M → N} {g : α →₀ M} {hf : f 0 = 0} {a : α} {b : M}
+    (hg : a ∉ g.support) : mapRange f hf (single a b + g) = single a (f b) + mapRange f hf g := by
+  ext e
+  obtain rfl | he := eq_or_ne e a
+  · rw [notMem_support_iff] at hg
+    simp_all
+  · simp [he]
+
+end Finsupp
+
+namespace AddMonoidAlgebra
+variable {R S : Type*} [Semiring R]
+
+@[simp] theorem coe_zero : ⇑(0 : R[S]) = 0 := rfl
+theorem zero_apply (x : S) : (0 : R[S]) x = 0 := rfl
+
+variable [Zero S]
+
+@[simp] theorem coe_one : ⇑(1 : R[S]) = single 0 1 := rfl
+
+theorem one_apply_zero : (1 : R[S]) 0 = 1 := by simp
+theorem one_apply_of_ne_zero {x : S} (hx : x ≠ 0) : (1 : R[S]) x = 0 := by simp [hx]
+
+end AddMonoidAlgebra
+
+namespace Nimber
+variable (b : Nimber) (hb : IsField b)
+
+open AddMonoidAlgebra
+
+/-! ### Nimbers as an `AddMonoidAlgebra` -/
+
+/-- Interpret a nimber `x` as a sum of powers of `b`, for `b` a field.
+
+This can be seen as a nimber specialization of the Cantor Normal form. -/
+def toAddMonoidAlgebra (x : Nimber) : hb.toSubfield[Ordinal] :=
+  (CNF.coeff b.val x.val).mapRange
+    (fun z ↦ if h : z < b.val then ⟨z, h⟩ else ⟨0, hb.pos⟩) (dif_pos hb.pos)
+
+@[simp]
+private theorem toAddMonoidAlgebra_apply (x : Nimber) (e : Ordinal) :
+    toAddMonoidAlgebra b hb x e = ⟨∗(CNF.coeff b.val x.val e), CNF.coeff_lt hb.one_lt _ e⟩ :=
+  dif_pos ..
+
+@[simp]
+theorem toAddMonoidAlgebra_zero : toAddMonoidAlgebra b hb 0 = 0 := by
+  ext; simp
+
+@[simp]
+theorem toAddMonoidAlgebra_one : toAddMonoidAlgebra b hb 1 = 1 := by
+  ext e
+  by_cases he : e = 0 <;> simp [he]
+
+/-! ### `AddMonoidAlgebra`s as nimbers -/
+
+/-- Add together powers of `b` to create a nimber. -/
+@[pp_nodot]
+def ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) : Nimber :=
+  ∗(CNF.eval b.val (x.mapRange (fun e ↦ e.1.val) rfl))
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+theorem ofAddMonoidAlgebra_zero : ofAddMonoidAlgebra b hb 0 = 0 := by
+  simp [ofAddMonoidAlgebra]
+
+@[simp]
+theorem ofAddMonoidAlgebra_one : ofAddMonoidAlgebra b hb 1 = 1 := by
+  simp [ofAddMonoidAlgebra, one_def]
+
+@[simp]
+theorem toAddMonoidAlgebra_ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) :
+    toAddMonoidAlgebra b hb (ofAddMonoidAlgebra b hb x) = x := by
+  ext e
+  simp only [ofAddMonoidAlgebra, toAddMonoidAlgebra_apply, val_of]
+  rw [CNF.coeff_eval (b := b.val) hb.one_lt] <;> simp
+
+@[simp]
+theorem ofAddMonoidAlgebra_toAddMonoidAlgebra (x : Nimber) :
+    ofAddMonoidAlgebra b hb (toAddMonoidAlgebra b hb x) = x := by
+  rw [ofAddMonoidAlgebra, of_eq_iff]
+  convert CNF.eval_coeff _ _
+  ext
+  simp
+
+theorem toAddMonoidAlgebra_injective : Function.Injective (toAddMonoidAlgebra b hb) :=
+  Function.LeftInverse.injective (ofAddMonoidAlgebra_toAddMonoidAlgebra b hb)
+
+theorem ofAddMonoidAlgebra_injective : Function.Injective (ofAddMonoidAlgebra b hb) :=
+  Function.LeftInverse.injective (toAddMonoidAlgebra_ofAddMonoidAlgebra b hb)
+
+@[simp]
+theorem toAddMonoidAlgebra_inj {x y} :
+    toAddMonoidAlgebra b hb x = toAddMonoidAlgebra b hb y ↔ x = y :=
+  (toAddMonoidAlgebra_injective b hb).eq_iff
+
+@[simp]
+theorem ofAddMonoidAlgebra_inj {x y} :
+    ofAddMonoidAlgebra b hb x = ofAddMonoidAlgebra b hb y ↔ x = y :=
+  (ofAddMonoidAlgebra_injective b hb).eq_iff
+
+set_option backward.isDefEq.respectTransparency false in
+theorem ofAddMonoidAlgebra_def (x : hb.toSubfield[Ordinal]) :
+    ofAddMonoidAlgebra b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
+  induction x using Finsupp.induction_on_max with
+  | zero => simp
+  | single_add o x f hf hx IH =>
+    rw [ofAddMonoidAlgebra, Finsupp.mapRange_single_add (by contrapose! hf; use o),
+      CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
+    · rw [Finsupp.sum_add_index' (by simp) (by simp [add_mul]), ← IH,
+        Finsupp.sum_single_index (by simp), mul_comm, ofAddMonoidAlgebra]
+    · simp
+    · apply CNF.eval_lt
+      · simp
+      · simpa using hf
+    · simpa using hf
+
+/-- `toAddMonoidAlgebra` as an `AddEquiv`. -/
+def toAddMonoidAlgebraIso : Nimber ≃+ hb.toSubfield[Ordinal] :=
+  sorry
+
+@[simp]
+theorem ofAddMonoidAlgebra_add (x y : hb.toSubfield[Ordinal]) :
+    ofAddMonoidAlgebra b hb (x + y) = ofAddMonoidAlgebra b hb x + ofAddMonoidAlgebra b hb y := by
+  simp_rw [ofAddMonoidAlgebra_def]
+  apply Finsupp.sum_add_index'
+  · simp
+  · simp [add_mul]
+
+theorem toAddMonoidAlgebra_add (x y : Nimber) :
+    toAddMonoidAlgebra b hb (x + y) = toAddMonoidAlgebra b hb x + toAddMonoidAlgebra b hb y := by
+  rw [← ofAddMonoidAlgebra_inj b hb]
+  sorry
+
+noncomputable def IsField.opow_basis {x : Nimber} (h : IsField x) :
+    Module.Basis Ordinal h.toSubfield Nimber :=
+  .mk (v := fun o ↦ ∗(x.val ^ o)) sorry sorry
+
+end Nimber
+end

From f125b3a97a2137de7be9008571911e676f91117a Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 07:12:02 -0600
Subject: [PATCH 02/12] there

---
 CombinatorialGames.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CombinatorialGames.lean b/CombinatorialGames.lean
index 513b89fa..374a60d2 100644
--- a/CombinatorialGames.lean
+++ b/CombinatorialGames.lean
@@ -30,6 +30,7 @@ import CombinatorialGames.NatOrdinal.Pow
 import CombinatorialGames.Nimber.Basic
 import CombinatorialGames.Nimber.Field
 import CombinatorialGames.Nimber.Nat
+import CombinatorialGames.Nimber.SimplestExtension.AddMonoidAlgebra
 import CombinatorialGames.Nimber.SimplestExtension.Algebraic
 import CombinatorialGames.Nimber.SimplestExtension.Basic
 import CombinatorialGames.Nimber.SimplestExtension.Closure

From 9e5726933c296448de6b1bec27320f326e6da8ad Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 07:33:41 -0600
Subject: [PATCH 03/12] finish

---
 CombinatorialGames.lean                       |   2 +-
 .../SimplestExtension/AddMonoidAlgebra.lean   | 185 ------------------
 2 files changed, 1 insertion(+), 186 deletions(-)
 delete mode 100644 CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean

diff --git a/CombinatorialGames.lean b/CombinatorialGames.lean
index 374a60d2..dcaea7d8 100644
--- a/CombinatorialGames.lean
+++ b/CombinatorialGames.lean
@@ -27,10 +27,10 @@ import CombinatorialGames.Mathlib.Small
 import CombinatorialGames.Mathlib.WithTop
 import CombinatorialGames.NatOrdinal.Basic
 import CombinatorialGames.NatOrdinal.Pow
+import CombinatorialGames.Nimber.AddMonoidAlgebra
 import CombinatorialGames.Nimber.Basic
 import CombinatorialGames.Nimber.Field
 import CombinatorialGames.Nimber.Nat
-import CombinatorialGames.Nimber.SimplestExtension.AddMonoidAlgebra
 import CombinatorialGames.Nimber.SimplestExtension.Algebraic
 import CombinatorialGames.Nimber.SimplestExtension.Basic
 import CombinatorialGames.Nimber.SimplestExtension.Closure
diff --git a/CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean b/CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean
deleted file mode 100644
index 371b409c..00000000
--- a/CombinatorialGames/Nimber/SimplestExtension/AddMonoidAlgebra.lean
+++ /dev/null
@@ -1,185 +0,0 @@
-module
-
-public import CombinatorialGames.Nimber.SimplestExtension.Basic
-public import Mathlib.Algebra.MonoidAlgebra.Defs
-public import Mathlib.LinearAlgebra.Basis.Basic
-public import Mathlib.SetTheory.Ordinal.CantorNormalForm
-
-public noncomputable section
-
-open Ordinal
-
-/-! ### For Mathlib -/
-
-namespace Ordinal.CNF
-
-@[simp]
-theorem CNF_one (b : Ordinal) : CNF b 1 = [(0, 1)] := by
-  obtain hb | hb := le_or_gt b 1
-  · exact CNF.of_le_one hb one_ne_zero
-  · exact CNF.of_lt one_ne_zero hb
-
-theorem coeff_lt {b : Ordinal} (hb : 1 < b) (o e : Ordinal) : coeff b o e < b := by
-  by_cases he : e ∈ (CNF b o).map Prod.fst
-  · rw [List.mem_map, Prod.exists] at he
-    obtain ⟨c, _, hc, rfl⟩ := he
-    rw [coeff_of_mem_CNF hc]
-    exact snd_lt hb hc
-  · rw [coeff_of_notMem_CNF he]
-    exact hb.pos
-
-@[simp]
-theorem coeff_one (b : Ordinal) : coeff b 1 = Finsupp.single 0 1 := by
-  ext e
-  obtain rfl | he := eq_or_ne e 0
-  · rw [Finsupp.single_eq_same]
-    apply coeff_of_mem_CNF
-    simp
-  · rw [coeff_of_notMem_CNF]
-    · simp [he]
-    · simpa
-
-end Ordinal.CNF
-
-namespace Finsupp
-variable {M N α : Type*} [AddZeroClass M] [AddZeroClass N]
-
-theorem mapRange_single_add {f : M → N} {g : α →₀ M} {hf : f 0 = 0} {a : α} {b : M}
-    (hg : a ∉ g.support) : mapRange f hf (single a b + g) = single a (f b) + mapRange f hf g := by
-  ext e
-  obtain rfl | he := eq_or_ne e a
-  · rw [notMem_support_iff] at hg
-    simp_all
-  · simp [he]
-
-end Finsupp
-
-namespace AddMonoidAlgebra
-variable {R S : Type*} [Semiring R]
-
-@[simp] theorem coe_zero : ⇑(0 : R[S]) = 0 := rfl
-theorem zero_apply (x : S) : (0 : R[S]) x = 0 := rfl
-
-variable [Zero S]
-
-@[simp] theorem coe_one : ⇑(1 : R[S]) = single 0 1 := rfl
-
-theorem one_apply_zero : (1 : R[S]) 0 = 1 := by simp
-theorem one_apply_of_ne_zero {x : S} (hx : x ≠ 0) : (1 : R[S]) x = 0 := by simp [hx]
-
-end AddMonoidAlgebra
-
-namespace Nimber
-variable (b : Nimber) (hb : IsField b)
-
-open AddMonoidAlgebra
-
-/-! ### Nimbers as an `AddMonoidAlgebra` -/
-
-/-- Interpret a nimber `x` as a sum of powers of `b`, for `b` a field.
-
-This can be seen as a nimber specialization of the Cantor Normal form. -/
-def toAddMonoidAlgebra (x : Nimber) : hb.toSubfield[Ordinal] :=
-  (CNF.coeff b.val x.val).mapRange
-    (fun z ↦ if h : z < b.val then ⟨z, h⟩ else ⟨0, hb.pos⟩) (dif_pos hb.pos)
-
-@[simp]
-private theorem toAddMonoidAlgebra_apply (x : Nimber) (e : Ordinal) :
-    toAddMonoidAlgebra b hb x e = ⟨∗(CNF.coeff b.val x.val e), CNF.coeff_lt hb.one_lt _ e⟩ :=
-  dif_pos ..
-
-@[simp]
-theorem toAddMonoidAlgebra_zero : toAddMonoidAlgebra b hb 0 = 0 := by
-  ext; simp
-
-@[simp]
-theorem toAddMonoidAlgebra_one : toAddMonoidAlgebra b hb 1 = 1 := by
-  ext e
-  by_cases he : e = 0 <;> simp [he]
-
-/-! ### `AddMonoidAlgebra`s as nimbers -/
-
-/-- Add together powers of `b` to create a nimber. -/
-@[pp_nodot]
-def ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) : Nimber :=
-  ∗(CNF.eval b.val (x.mapRange (fun e ↦ e.1.val) rfl))
-
-set_option backward.isDefEq.respectTransparency false in
-@[simp]
-theorem ofAddMonoidAlgebra_zero : ofAddMonoidAlgebra b hb 0 = 0 := by
-  simp [ofAddMonoidAlgebra]
-
-@[simp]
-theorem ofAddMonoidAlgebra_one : ofAddMonoidAlgebra b hb 1 = 1 := by
-  simp [ofAddMonoidAlgebra, one_def]
-
-@[simp]
-theorem toAddMonoidAlgebra_ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) :
-    toAddMonoidAlgebra b hb (ofAddMonoidAlgebra b hb x) = x := by
-  ext e
-  simp only [ofAddMonoidAlgebra, toAddMonoidAlgebra_apply, val_of]
-  rw [CNF.coeff_eval (b := b.val) hb.one_lt] <;> simp
-
-@[simp]
-theorem ofAddMonoidAlgebra_toAddMonoidAlgebra (x : Nimber) :
-    ofAddMonoidAlgebra b hb (toAddMonoidAlgebra b hb x) = x := by
-  rw [ofAddMonoidAlgebra, of_eq_iff]
-  convert CNF.eval_coeff _ _
-  ext
-  simp
-
-theorem toAddMonoidAlgebra_injective : Function.Injective (toAddMonoidAlgebra b hb) :=
-  Function.LeftInverse.injective (ofAddMonoidAlgebra_toAddMonoidAlgebra b hb)
-
-theorem ofAddMonoidAlgebra_injective : Function.Injective (ofAddMonoidAlgebra b hb) :=
-  Function.LeftInverse.injective (toAddMonoidAlgebra_ofAddMonoidAlgebra b hb)
-
-@[simp]
-theorem toAddMonoidAlgebra_inj {x y} :
-    toAddMonoidAlgebra b hb x = toAddMonoidAlgebra b hb y ↔ x = y :=
-  (toAddMonoidAlgebra_injective b hb).eq_iff
-
-@[simp]
-theorem ofAddMonoidAlgebra_inj {x y} :
-    ofAddMonoidAlgebra b hb x = ofAddMonoidAlgebra b hb y ↔ x = y :=
-  (ofAddMonoidAlgebra_injective b hb).eq_iff
-
-set_option backward.isDefEq.respectTransparency false in
-theorem ofAddMonoidAlgebra_def (x : hb.toSubfield[Ordinal]) :
-    ofAddMonoidAlgebra b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
-  induction x using Finsupp.induction_on_max with
-  | zero => simp
-  | single_add o x f hf hx IH =>
-    rw [ofAddMonoidAlgebra, Finsupp.mapRange_single_add (by contrapose! hf; use o),
-      CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
-    · rw [Finsupp.sum_add_index' (by simp) (by simp [add_mul]), ← IH,
-        Finsupp.sum_single_index (by simp), mul_comm, ofAddMonoidAlgebra]
-    · simp
-    · apply CNF.eval_lt
-      · simp
-      · simpa using hf
-    · simpa using hf
-
-/-- `toAddMonoidAlgebra` as an `AddEquiv`. -/
-def toAddMonoidAlgebraIso : Nimber ≃+ hb.toSubfield[Ordinal] :=
-  sorry
-
-@[simp]
-theorem ofAddMonoidAlgebra_add (x y : hb.toSubfield[Ordinal]) :
-    ofAddMonoidAlgebra b hb (x + y) = ofAddMonoidAlgebra b hb x + ofAddMonoidAlgebra b hb y := by
-  simp_rw [ofAddMonoidAlgebra_def]
-  apply Finsupp.sum_add_index'
-  · simp
-  · simp [add_mul]
-
-theorem toAddMonoidAlgebra_add (x y : Nimber) :
-    toAddMonoidAlgebra b hb (x + y) = toAddMonoidAlgebra b hb x + toAddMonoidAlgebra b hb y := by
-  rw [← ofAddMonoidAlgebra_inj b hb]
-  sorry
-
-noncomputable def IsField.opow_basis {x : Nimber} (h : IsField x) :
-    Module.Basis Ordinal h.toSubfield Nimber :=
-  .mk (v := fun o ↦ ∗(x.val ^ o)) sorry sorry
-
-end Nimber
-end

From 9cc119ec806fa50d7fb20480d21658d840eec87c Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 07:34:16 -0600
Subject: [PATCH 04/12] is this going to work now

---
 .../Nimber/AddMonoidAlgebra.lean              | 218 ++++++++++++++++++
 1 file changed, 218 insertions(+)
 create mode 100644 CombinatorialGames/Nimber/AddMonoidAlgebra.lean

diff --git a/CombinatorialGames/Nimber/AddMonoidAlgebra.lean b/CombinatorialGames/Nimber/AddMonoidAlgebra.lean
new file mode 100644
index 00000000..a29c85e6
--- /dev/null
+++ b/CombinatorialGames/Nimber/AddMonoidAlgebra.lean
@@ -0,0 +1,218 @@
+/-
+Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import CombinatorialGames.Nimber.SimplestExtension.Basic
+public import Mathlib.Algebra.MonoidAlgebra.Defs
+public import Mathlib.LinearAlgebra.Basis.Basic
+
+import Mathlib.SetTheory.Ordinal.CantorNormalForm
+
+/-!
+# Nimbers as an `AddMonoidAlgebra`
+
+We prove that if `b` is a field, then the base-`b` Cantor normal form of a nimber respects addition,
+when viewed as a formal sum of powers of `b`.
+-/
+
+universe u
+
+/-! ### For Mathlib -/
+
+namespace Ordinal.CNF
+
+@[simp]
+theorem CNF_one (b : Ordinal) : CNF b 1 = [(0, 1)] := by
+  obtain hb | hb := le_or_gt b 1
+  · exact CNF.of_le_one hb one_ne_zero
+  · exact CNF.of_lt one_ne_zero hb
+
+theorem coeff_lt {b : Ordinal} (hb : 1 < b) (o e : Ordinal) : coeff b o e < b := by
+  by_cases he : e ∈ (CNF b o).map Prod.fst
+  · rw [List.mem_map, Prod.exists] at he
+    obtain ⟨c, _, hc, rfl⟩ := he
+    rw [coeff_of_mem_CNF hc]
+    exact snd_lt hb hc
+  · rw [coeff_of_notMem_CNF he]
+    exact hb.pos
+
+@[simp]
+theorem coeff_one (b : Ordinal) : coeff b 1 = Finsupp.single 0 1 := by
+  ext e
+  obtain rfl | he := eq_or_ne e 0
+  · rw [Finsupp.single_eq_same]
+    apply coeff_of_mem_CNF
+    simp
+  · rw [coeff_of_notMem_CNF]
+    · simp [he]
+    · simpa
+
+end Ordinal.CNF
+
+namespace Finsupp
+variable {M N α : Type*} [AddZeroClass M] [AddZeroClass N]
+
+theorem mapRange_single_add {f : M → N} {g : α →₀ M} {hf : f 0 = 0} {a : α} {b : M}
+    (hg : a ∉ g.support) : mapRange f hf (single a b + g) = single a (f b) + mapRange f hf g := by
+  ext e
+  obtain rfl | he := eq_or_ne e a
+  · rw [notMem_support_iff] at hg
+    simp_all
+  · simp [he]
+
+end Finsupp
+
+namespace AddMonoidAlgebra
+variable {R S : Type*} [Semiring R]
+
+@[simp] theorem coe_zero : ⇑(0 : R[S]) = 0 := rfl
+theorem zero_apply (x : S) : (0 : R[S]) x = 0 := rfl
+
+variable [Zero S]
+
+@[simp] theorem coe_one : ⇑(1 : R[S]) = single 0 1 := rfl
+
+theorem one_apply_zero : (1 : R[S]) 0 = 1 := by simp
+theorem one_apply_of_ne_zero {x : S} (hx : x ≠ 0) : (1 : R[S]) x = 0 := by simp [hx]
+
+end AddMonoidAlgebra
+
+public noncomputable section
+
+namespace Nimber
+variable (b : Nimber) (hb : IsField b)
+
+open AddMonoidAlgebra Ordinal
+
+/-! ### Nimbers as an `AddMonoidAlgebra` -/
+
+/-- Interpret a nimber `x` as a sum of powers of `b`, for `b` a field.
+
+This can be seen as a nimber specialization of the Cantor Normal form. -/
+def toAddMonoidAlgebra (x : Nimber) : hb.toSubfield[Ordinal] :=
+  (CNF.coeff b.val x.val).mapRange
+    (fun z ↦ if h : z < b.val then ⟨z, h⟩ else ⟨0, hb.pos⟩) (dif_pos hb.pos)
+
+@[simp]
+private theorem toAddMonoidAlgebra_apply (x : Nimber) (e : Ordinal) :
+    toAddMonoidAlgebra b hb x e = ⟨∗(CNF.coeff b.val x.val e), CNF.coeff_lt hb.one_lt _ e⟩ :=
+  dif_pos ..
+
+@[simp]
+theorem toAddMonoidAlgebra_zero : toAddMonoidAlgebra b hb 0 = 0 := by
+  ext; simp
+
+@[simp]
+theorem toAddMonoidAlgebra_one : toAddMonoidAlgebra b hb 1 = 1 := by
+  ext e
+  by_cases he : e = 0 <;> simp [he]
+
+/-! ### `AddMonoidAlgebra`s as nimbers -/
+
+/-- Add together powers of `b` to create a nimber. -/
+@[pp_nodot]
+def ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) : Nimber :=
+  ∗(CNF.eval b.val (x.mapRange (fun e ↦ e.1.val) rfl))
+
+set_option backward.isDefEq.respectTransparency false in
+@[simp]
+theorem ofAddMonoidAlgebra_zero : ofAddMonoidAlgebra b hb 0 = 0 := by
+  simp [ofAddMonoidAlgebra]
+
+@[simp]
+theorem ofAddMonoidAlgebra_one : ofAddMonoidAlgebra b hb 1 = 1 := by
+  simp [ofAddMonoidAlgebra, one_def]
+
+/-! ### Conversions -/
+
+@[simp]
+theorem toAddMonoidAlgebra_ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) :
+    toAddMonoidAlgebra b hb (ofAddMonoidAlgebra b hb x) = x := by
+  ext e
+  simp only [ofAddMonoidAlgebra, toAddMonoidAlgebra_apply, val_of]
+  rw [CNF.coeff_eval (b := b.val) hb.one_lt] <;> simp
+
+@[simp]
+theorem ofAddMonoidAlgebra_toAddMonoidAlgebra (x : Nimber) :
+    ofAddMonoidAlgebra b hb (toAddMonoidAlgebra b hb x) = x := by
+  rw [ofAddMonoidAlgebra, of_eq_iff]
+  convert CNF.eval_coeff _ _
+  ext
+  simp
+
+theorem toAddMonoidAlgebra_injective : Function.Injective (toAddMonoidAlgebra b hb) :=
+  Function.LeftInverse.injective (ofAddMonoidAlgebra_toAddMonoidAlgebra b hb)
+
+theorem ofAddMonoidAlgebra_injective : Function.Injective (ofAddMonoidAlgebra b hb) :=
+  Function.LeftInverse.injective (toAddMonoidAlgebra_ofAddMonoidAlgebra b hb)
+
+@[simp]
+theorem toAddMonoidAlgebra_inj {x y} :
+    toAddMonoidAlgebra b hb x = toAddMonoidAlgebra b hb y ↔ x = y :=
+  (toAddMonoidAlgebra_injective b hb).eq_iff
+
+@[simp]
+theorem ofAddMonoidAlgebra_inj {x y} :
+    ofAddMonoidAlgebra b hb x = ofAddMonoidAlgebra b hb y ↔ x = y :=
+  (ofAddMonoidAlgebra_injective b hb).eq_iff
+
+set_option backward.isDefEq.respectTransparency false in
+theorem ofAddMonoidAlgebra_def (x : hb.toSubfield[Ordinal]) :
+    ofAddMonoidAlgebra b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
+  induction x using Finsupp.induction_on_max with
+  | zero => simp
+  | single_add o x f hf hx IH =>
+    rw [ofAddMonoidAlgebra, Finsupp.mapRange_single_add (by contrapose! hf; use o),
+      CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
+    · rw [Finsupp.sum_add_index' (by simp) (by simp [add_mul]), ← IH,
+        Finsupp.sum_single_index (by simp), mul_comm, ofAddMonoidAlgebra]
+    · simp
+    · apply CNF.eval_lt
+      · simp
+      · simpa using hf
+    · simpa using hf
+
+@[simp]
+theorem ofAddMonoidAlgebra_add (x y : hb.toSubfield[Ordinal]) :
+    ofAddMonoidAlgebra b hb (x + y) = ofAddMonoidAlgebra b hb x + ofAddMonoidAlgebra b hb y := by
+  simp_rw [ofAddMonoidAlgebra_def]
+  apply Finsupp.sum_add_index'
+  · simp
+  · simp [add_mul]
+
+/-- `toAddMonoidAlgebra` as an `AddEquiv`. -/
+@[expose, simps!]
+def toAddMonoidAlgebraAddEquiv : Nimber ≃+ hb.toSubfield[Ordinal] :=
+  .symm {
+    toFun := ofAddMonoidAlgebra b hb
+    invFun := toAddMonoidAlgebra b hb
+    map_add' := ofAddMonoidAlgebra_add b hb
+    left_inv := toAddMonoidAlgebra_ofAddMonoidAlgebra b hb
+    right_inv := ofAddMonoidAlgebra_toAddMonoidAlgebra b hb
+  }
+
+@[simp]
+theorem toAddMonoidAlgebra_add (x y : Nimber) :
+    toAddMonoidAlgebra b hb (x + y) = toAddMonoidAlgebra b hb x + toAddMonoidAlgebra b hb y :=
+  (toAddMonoidAlgebraAddEquiv b hb).map_add x y
+
+/-! ### Basis -/
+
+/-- `toAddMonoidAlgebra` as a `LinearEquiv`. -/
+@[expose, simps!]
+def toAddMonoidAlgebraLinearEquiv : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :=
+  .symm {
+    map_smul' := by simp [ofAddMonoidAlgebra_def, Finsupp.sum_smul_index, Finsupp.smul_sum,
+      Subfield.smul_def, mul_assoc]
+    __ := (toAddMonoidAlgebraAddEquiv b hb).symm
+  }
+
+/-- Ordinal powers of `b` as a basis for `Nimber`. -/
+def IsField.opow_basis : Module.Basis Ordinal.{u} hb.toSubfield Nimber where
+  repr := toAddMonoidAlgebraLinearEquiv b hb
+
+end Nimber
+end

From 306f1cd8cb1cd2293336a16f0a2d74c4946c18f9 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 08:53:46 -0600
Subject: [PATCH 05/12] tweak

---
 .../Nimber/AddMonoidAlgebra.lean              | 218 ------------------
 1 file changed, 218 deletions(-)
 delete mode 100644 CombinatorialGames/Nimber/AddMonoidAlgebra.lean

diff --git a/CombinatorialGames/Nimber/AddMonoidAlgebra.lean b/CombinatorialGames/Nimber/AddMonoidAlgebra.lean
deleted file mode 100644
index a29c85e6..00000000
--- a/CombinatorialGames/Nimber/AddMonoidAlgebra.lean
+++ /dev/null
@@ -1,218 +0,0 @@
-/-
-Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Violeta Hernández Palacios
--/
-module
-
-public import CombinatorialGames.Nimber.SimplestExtension.Basic
-public import Mathlib.Algebra.MonoidAlgebra.Defs
-public import Mathlib.LinearAlgebra.Basis.Basic
-
-import Mathlib.SetTheory.Ordinal.CantorNormalForm
-
-/-!
-# Nimbers as an `AddMonoidAlgebra`
-
-We prove that if `b` is a field, then the base-`b` Cantor normal form of a nimber respects addition,
-when viewed as a formal sum of powers of `b`.
--/
-
-universe u
-
-/-! ### For Mathlib -/
-
-namespace Ordinal.CNF
-
-@[simp]
-theorem CNF_one (b : Ordinal) : CNF b 1 = [(0, 1)] := by
-  obtain hb | hb := le_or_gt b 1
-  · exact CNF.of_le_one hb one_ne_zero
-  · exact CNF.of_lt one_ne_zero hb
-
-theorem coeff_lt {b : Ordinal} (hb : 1 < b) (o e : Ordinal) : coeff b o e < b := by
-  by_cases he : e ∈ (CNF b o).map Prod.fst
-  · rw [List.mem_map, Prod.exists] at he
-    obtain ⟨c, _, hc, rfl⟩ := he
-    rw [coeff_of_mem_CNF hc]
-    exact snd_lt hb hc
-  · rw [coeff_of_notMem_CNF he]
-    exact hb.pos
-
-@[simp]
-theorem coeff_one (b : Ordinal) : coeff b 1 = Finsupp.single 0 1 := by
-  ext e
-  obtain rfl | he := eq_or_ne e 0
-  · rw [Finsupp.single_eq_same]
-    apply coeff_of_mem_CNF
-    simp
-  · rw [coeff_of_notMem_CNF]
-    · simp [he]
-    · simpa
-
-end Ordinal.CNF
-
-namespace Finsupp
-variable {M N α : Type*} [AddZeroClass M] [AddZeroClass N]
-
-theorem mapRange_single_add {f : M → N} {g : α →₀ M} {hf : f 0 = 0} {a : α} {b : M}
-    (hg : a ∉ g.support) : mapRange f hf (single a b + g) = single a (f b) + mapRange f hf g := by
-  ext e
-  obtain rfl | he := eq_or_ne e a
-  · rw [notMem_support_iff] at hg
-    simp_all
-  · simp [he]
-
-end Finsupp
-
-namespace AddMonoidAlgebra
-variable {R S : Type*} [Semiring R]
-
-@[simp] theorem coe_zero : ⇑(0 : R[S]) = 0 := rfl
-theorem zero_apply (x : S) : (0 : R[S]) x = 0 := rfl
-
-variable [Zero S]
-
-@[simp] theorem coe_one : ⇑(1 : R[S]) = single 0 1 := rfl
-
-theorem one_apply_zero : (1 : R[S]) 0 = 1 := by simp
-theorem one_apply_of_ne_zero {x : S} (hx : x ≠ 0) : (1 : R[S]) x = 0 := by simp [hx]
-
-end AddMonoidAlgebra
-
-public noncomputable section
-
-namespace Nimber
-variable (b : Nimber) (hb : IsField b)
-
-open AddMonoidAlgebra Ordinal
-
-/-! ### Nimbers as an `AddMonoidAlgebra` -/
-
-/-- Interpret a nimber `x` as a sum of powers of `b`, for `b` a field.
-
-This can be seen as a nimber specialization of the Cantor Normal form. -/
-def toAddMonoidAlgebra (x : Nimber) : hb.toSubfield[Ordinal] :=
-  (CNF.coeff b.val x.val).mapRange
-    (fun z ↦ if h : z < b.val then ⟨z, h⟩ else ⟨0, hb.pos⟩) (dif_pos hb.pos)
-
-@[simp]
-private theorem toAddMonoidAlgebra_apply (x : Nimber) (e : Ordinal) :
-    toAddMonoidAlgebra b hb x e = ⟨∗(CNF.coeff b.val x.val e), CNF.coeff_lt hb.one_lt _ e⟩ :=
-  dif_pos ..
-
-@[simp]
-theorem toAddMonoidAlgebra_zero : toAddMonoidAlgebra b hb 0 = 0 := by
-  ext; simp
-
-@[simp]
-theorem toAddMonoidAlgebra_one : toAddMonoidAlgebra b hb 1 = 1 := by
-  ext e
-  by_cases he : e = 0 <;> simp [he]
-
-/-! ### `AddMonoidAlgebra`s as nimbers -/
-
-/-- Add together powers of `b` to create a nimber. -/
-@[pp_nodot]
-def ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) : Nimber :=
-  ∗(CNF.eval b.val (x.mapRange (fun e ↦ e.1.val) rfl))
-
-set_option backward.isDefEq.respectTransparency false in
-@[simp]
-theorem ofAddMonoidAlgebra_zero : ofAddMonoidAlgebra b hb 0 = 0 := by
-  simp [ofAddMonoidAlgebra]
-
-@[simp]
-theorem ofAddMonoidAlgebra_one : ofAddMonoidAlgebra b hb 1 = 1 := by
-  simp [ofAddMonoidAlgebra, one_def]
-
-/-! ### Conversions -/
-
-@[simp]
-theorem toAddMonoidAlgebra_ofAddMonoidAlgebra (x : hb.toSubfield[Ordinal]) :
-    toAddMonoidAlgebra b hb (ofAddMonoidAlgebra b hb x) = x := by
-  ext e
-  simp only [ofAddMonoidAlgebra, toAddMonoidAlgebra_apply, val_of]
-  rw [CNF.coeff_eval (b := b.val) hb.one_lt] <;> simp
-
-@[simp]
-theorem ofAddMonoidAlgebra_toAddMonoidAlgebra (x : Nimber) :
-    ofAddMonoidAlgebra b hb (toAddMonoidAlgebra b hb x) = x := by
-  rw [ofAddMonoidAlgebra, of_eq_iff]
-  convert CNF.eval_coeff _ _
-  ext
-  simp
-
-theorem toAddMonoidAlgebra_injective : Function.Injective (toAddMonoidAlgebra b hb) :=
-  Function.LeftInverse.injective (ofAddMonoidAlgebra_toAddMonoidAlgebra b hb)
-
-theorem ofAddMonoidAlgebra_injective : Function.Injective (ofAddMonoidAlgebra b hb) :=
-  Function.LeftInverse.injective (toAddMonoidAlgebra_ofAddMonoidAlgebra b hb)
-
-@[simp]
-theorem toAddMonoidAlgebra_inj {x y} :
-    toAddMonoidAlgebra b hb x = toAddMonoidAlgebra b hb y ↔ x = y :=
-  (toAddMonoidAlgebra_injective b hb).eq_iff
-
-@[simp]
-theorem ofAddMonoidAlgebra_inj {x y} :
-    ofAddMonoidAlgebra b hb x = ofAddMonoidAlgebra b hb y ↔ x = y :=
-  (ofAddMonoidAlgebra_injective b hb).eq_iff
-
-set_option backward.isDefEq.respectTransparency false in
-theorem ofAddMonoidAlgebra_def (x : hb.toSubfield[Ordinal]) :
-    ofAddMonoidAlgebra b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
-  induction x using Finsupp.induction_on_max with
-  | zero => simp
-  | single_add o x f hf hx IH =>
-    rw [ofAddMonoidAlgebra, Finsupp.mapRange_single_add (by contrapose! hf; use o),
-      CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
-    · rw [Finsupp.sum_add_index' (by simp) (by simp [add_mul]), ← IH,
-        Finsupp.sum_single_index (by simp), mul_comm, ofAddMonoidAlgebra]
-    · simp
-    · apply CNF.eval_lt
-      · simp
-      · simpa using hf
-    · simpa using hf
-
-@[simp]
-theorem ofAddMonoidAlgebra_add (x y : hb.toSubfield[Ordinal]) :
-    ofAddMonoidAlgebra b hb (x + y) = ofAddMonoidAlgebra b hb x + ofAddMonoidAlgebra b hb y := by
-  simp_rw [ofAddMonoidAlgebra_def]
-  apply Finsupp.sum_add_index'
-  · simp
-  · simp [add_mul]
-
-/-- `toAddMonoidAlgebra` as an `AddEquiv`. -/
-@[expose, simps!]
-def toAddMonoidAlgebraAddEquiv : Nimber ≃+ hb.toSubfield[Ordinal] :=
-  .symm {
-    toFun := ofAddMonoidAlgebra b hb
-    invFun := toAddMonoidAlgebra b hb
-    map_add' := ofAddMonoidAlgebra_add b hb
-    left_inv := toAddMonoidAlgebra_ofAddMonoidAlgebra b hb
-    right_inv := ofAddMonoidAlgebra_toAddMonoidAlgebra b hb
-  }
-
-@[simp]
-theorem toAddMonoidAlgebra_add (x y : Nimber) :
-    toAddMonoidAlgebra b hb (x + y) = toAddMonoidAlgebra b hb x + toAddMonoidAlgebra b hb y :=
-  (toAddMonoidAlgebraAddEquiv b hb).map_add x y
-
-/-! ### Basis -/
-
-/-- `toAddMonoidAlgebra` as a `LinearEquiv`. -/
-@[expose, simps!]
-def toAddMonoidAlgebraLinearEquiv : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :=
-  .symm {
-    map_smul' := by simp [ofAddMonoidAlgebra_def, Finsupp.sum_smul_index, Finsupp.smul_sum,
-      Subfield.smul_def, mul_assoc]
-    __ := (toAddMonoidAlgebraAddEquiv b hb).symm
-  }
-
-/-- Ordinal powers of `b` as a basis for `Nimber`. -/
-def IsField.opow_basis : Module.Basis Ordinal.{u} hb.toSubfield Nimber where
-  repr := toAddMonoidAlgebraLinearEquiv b hb
-
-end Nimber
-end

From 8d20d0e7942461a29a13a697073c119f5af1b52f Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 08:54:58 -0600
Subject: [PATCH 06/12] fix

---
 CombinatorialGames/Nimber/Finsupp.lean | 173 +++++++++++++++++++++++++
 1 file changed, 173 insertions(+)
 create mode 100644 CombinatorialGames/Nimber/Finsupp.lean

diff --git a/CombinatorialGames/Nimber/Finsupp.lean b/CombinatorialGames/Nimber/Finsupp.lean
new file mode 100644
index 00000000..b643e7a0
--- /dev/null
+++ b/CombinatorialGames/Nimber/Finsupp.lean
@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import CombinatorialGames.Nimber.SimplestExtension.Basic
+public import Mathlib.LinearAlgebra.Basis.Defs
+
+import Mathlib.SetTheory.Ordinal.CantorNormalForm
+
+/-!
+# Nimbers as finitely supported functions
+
+We prove that if `b` is a field, then the base-`b` Cantor normal form of a nimber respects addition,
+when viewed as a formal sum of powers of `b`.
+-/
+
+universe u
+
+/-! ### For Mathlib -/
+
+namespace Ordinal.CNF
+
+theorem coeff_lt {b : Ordinal} (hb : 1 < b) (o e : Ordinal) : coeff b o e < b := by
+  by_cases he : e ∈ (CNF b o).map Prod.fst
+  · rw [List.mem_map, Prod.exists] at he
+    obtain ⟨c, _, hc, rfl⟩ := he
+    rw [coeff_of_mem_CNF hc]
+    exact snd_lt hb hc
+  · rw [coeff_of_notMem_CNF he]
+    exact hb.pos
+
+end Ordinal.CNF
+
+namespace Finsupp
+variable {M N α : Type*} [AddZeroClass M] [AddZeroClass N]
+
+theorem mapRange_single_add {f : M → N} {g : α →₀ M} {hf : f 0 = 0} {a : α} {b : M}
+    (hg : a ∉ g.support) : mapRange f hf (single a b + g) = single a (f b) + mapRange f hf g := by
+  ext e
+  obtain rfl | he := eq_or_ne e a
+  · rw [notMem_support_iff] at hg
+    simp_all
+  · simp [he]
+
+end Finsupp
+
+public noncomputable section
+
+namespace Nimber
+variable (b : Nimber) (hb : IsField b)
+
+open Finsupp Ordinal
+
+/-- `toFinsupp b hb x e` returns the coefficient of `b ^ e` in `x`. This is a specialization of
+`Ordinal.CNF.coeff`. -/
+@[pp_nodot]
+def toFinsupp (x : Nimber) : Ordinal →₀ hb.toSubfield :=
+  (CNF.coeff b.val x.val).mapRange
+    (fun z ↦ if h : z < b.val then ⟨z, h⟩ else 0) (dif_pos hb.pos)
+
+@[simp]
+private theorem toFinsupp_apply (x : Nimber) (e : Ordinal) :
+    toFinsupp b hb x e = ⟨∗(CNF.coeff b.val x.val e), CNF.coeff_lt hb.one_lt _ e⟩ :=
+  dif_pos ..
+
+@[simp]
+theorem toFinsupp_zero : toFinsupp b hb 0 = 0 := by
+  ext; simp
+
+/-- Add a linear combination of ordinal powers of `b` to create a nimber. This is a specialization
+of `Ordinal.CNF.eval`. -/
+@[pp_nodot]
+def ofFinsupp (x : Ordinal →₀ hb.toSubfield) : Nimber :=
+  ∗(CNF.eval b.val (x.mapRange (fun e ↦ e.1.val) rfl))
+
+@[simp]
+theorem ofFinsupp_zero : ofFinsupp b hb 0 = 0 := by
+  simp [ofFinsupp]
+
+@[simp]
+theorem toFinsupp_ofFinsupp (x) : toFinsupp b hb (ofFinsupp b hb x) = x := by
+  ext e
+  simp only [ofFinsupp, toFinsupp_apply, val_of]
+  rw [CNF.coeff_eval (b := b.val) hb.one_lt] <;> simp
+
+@[simp]
+theorem ofFinsupp_toFinsupp (x) : ofFinsupp b hb (toFinsupp b hb x) = x := by
+  rw [ofFinsupp, of_eq_iff]
+  convert CNF.eval_coeff ..
+  ext
+  simp
+
+theorem toFinsupp_injective : Function.Injective (toFinsupp b hb) :=
+  Function.LeftInverse.injective (ofFinsupp_toFinsupp b hb)
+
+theorem ofFinsupp_injective : Function.Injective (ofFinsupp b hb) :=
+  Function.LeftInverse.injective (toFinsupp_ofFinsupp b hb)
+
+@[simp]
+theorem toFinsupp_inj {x y} : toFinsupp b hb x = toFinsupp b hb y ↔ x = y :=
+  (toFinsupp_injective b hb).eq_iff
+
+@[simp]
+theorem ofFinsupp_inj {x y} : ofFinsupp b hb x = ofFinsupp b hb y ↔ x = y :=
+  (ofFinsupp_injective b hb).eq_iff
+
+set_option backward.isDefEq.respectTransparency false in
+theorem ofFinsupp_def (x) : ofFinsupp b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
+  induction x using Finsupp.induction_on_max with
+  | zero => simp
+  | single_add o x f hf hx IH =>
+    rw [ofFinsupp, Finsupp.mapRange_single_add (by contrapose! hf; use o),
+      CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
+    · rw [Finsupp.sum_add_index' (by simp) (by simp [add_mul]), ← IH,
+        Finsupp.sum_single_index (by simp), mul_comm, ofFinsupp]
+    · simp
+    · apply CNF.eval_lt
+      · simp
+      · simpa using hf
+    · simpa using hf
+
+@[simp]
+theorem ofFinsupp_single (x y) : ofFinsupp b hb (single x y) = y * ∗(b.val ^ x) := by
+  simp [ofFinsupp_def]
+
+@[simp]
+theorem toFinsupp_opow_mul (o : Ordinal) {x : Nimber} (hx : x < b) :
+    toFinsupp b hb (x * ∗(b.val ^ o)) = single o ⟨x, hx⟩ := by
+  simp [← ofFinsupp_inj]
+
+@[simp]
+theorem toFinsupp_opow (o : Ordinal) : toFinsupp b hb (∗(b.val ^ o)) = single o 1 := by
+  simpa using toFinsupp_opow_mul b hb o hb.one_lt
+
+@[simp]
+theorem toFinsupp_one : toFinsupp b hb 1 = single 0 1 := by
+  simpa using toFinsupp_opow b hb 0
+
+/-- `toFinsupp` as a `LinearEquiv`. -/
+@[expose, simps!]
+def toFinsuppAddIso : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :=
+  .symm {
+    toFun := ofFinsupp b hb
+    invFun := toFinsupp b hb
+    left_inv := toFinsupp_ofFinsupp b hb
+    right_inv := ofFinsupp_toFinsupp b hb
+    map_add' x y := by
+      simp_rw [ofFinsupp_def]
+      apply Finsupp.sum_add_index'
+      · simp
+      · simp [add_mul]
+    map_smul' := by
+      simp [ofFinsupp_def, Finsupp.sum_smul_index, Finsupp.smul_sum, Subfield.smul_def, mul_assoc]
+  }
+
+@[simp]
+theorem toFinsupp_add (x y) : toFinsupp b hb (x + y) = toFinsupp b hb x + toFinsupp b hb y :=
+  (toFinsuppAddIso b hb).map_add x y
+
+@[simp]
+theorem ofFinsupp_add (x y) : ofFinsupp b hb (x + y) = ofFinsupp b hb x + ofFinsupp b hb y :=
+  (toFinsuppAddIso b hb).symm.map_add x y
+
+/-- Ordinal powers of `b` form a basis for `Nimber`. -/
+@[expose, simps!]
+def IsField.opow_basis : Module.Basis Ordinal.{u} hb.toSubfield Nimber where
+  repr := toFinsuppAddIso b hb
+
+end Nimber
+end

From fd0cbb8111015d10ccaee2a51dad8209afa4c1cc Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 08:55:10 -0600
Subject: [PATCH 07/12] fix?

---
 CombinatorialGames.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CombinatorialGames.lean b/CombinatorialGames.lean
index dcaea7d8..bb633f7e 100644
--- a/CombinatorialGames.lean
+++ b/CombinatorialGames.lean
@@ -27,9 +27,9 @@ import CombinatorialGames.Mathlib.Small
 import CombinatorialGames.Mathlib.WithTop
 import CombinatorialGames.NatOrdinal.Basic
 import CombinatorialGames.NatOrdinal.Pow
-import CombinatorialGames.Nimber.AddMonoidAlgebra
 import CombinatorialGames.Nimber.Basic
 import CombinatorialGames.Nimber.Field
+import CombinatorialGames.Nimber.Finsupp
 import CombinatorialGames.Nimber.Nat
 import CombinatorialGames.Nimber.SimplestExtension.Algebraic
 import CombinatorialGames.Nimber.SimplestExtension.Basic

From b72aaf2f6e605627cf08f25feaab18382ec7c365 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 09:43:24 -0600
Subject: [PATCH 08/12] fix names

---
 CombinatorialGames/Nimber/Finsupp.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/CombinatorialGames/Nimber/Finsupp.lean b/CombinatorialGames/Nimber/Finsupp.lean
index b643e7a0..0a38bab1 100644
--- a/CombinatorialGames/Nimber/Finsupp.lean
+++ b/CombinatorialGames/Nimber/Finsupp.lean
@@ -141,7 +141,7 @@ theorem toFinsupp_one : toFinsupp b hb 1 = single 0 1 := by
 
 /-- `toFinsupp` as a `LinearEquiv`. -/
 @[expose, simps!]
-def toFinsuppAddIso : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :=
+def toFinsuppIso : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :=
   .symm {
     toFun := ofFinsupp b hb
     invFun := toFinsupp b hb
@@ -158,16 +158,16 @@ def toFinsuppAddIso : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield
 
 @[simp]
 theorem toFinsupp_add (x y) : toFinsupp b hb (x + y) = toFinsupp b hb x + toFinsupp b hb y :=
-  (toFinsuppAddIso b hb).map_add x y
+  (toFinsuppIso b hb).map_add x y
 
 @[simp]
 theorem ofFinsupp_add (x y) : ofFinsupp b hb (x + y) = ofFinsupp b hb x + ofFinsupp b hb y :=
-  (toFinsuppAddIso b hb).symm.map_add x y
+  (toFinsuppIso b hb).symm.map_add x y
 
 /-- Ordinal powers of `b` form a basis for `Nimber`. -/
 @[expose, simps!]
 def IsField.opow_basis : Module.Basis Ordinal.{u} hb.toSubfield Nimber where
-  repr := toFinsuppAddIso b hb
+  repr := toFinsuppIso b hb
 
 end Nimber
 end

From ca284b78eada0e028239caa26ef4855475e52ec1 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 5 Mar 2026 09:48:43 -0600
Subject: [PATCH 09/12] golf

---
 CombinatorialGames/Nimber/Finsupp.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/CombinatorialGames/Nimber/Finsupp.lean b/CombinatorialGames/Nimber/Finsupp.lean
index 0a38bab1..f22adb0e 100644
--- a/CombinatorialGames/Nimber/Finsupp.lean
+++ b/CombinatorialGames/Nimber/Finsupp.lean
@@ -109,13 +109,13 @@ theorem ofFinsupp_inj {x y} : ofFinsupp b hb x = ofFinsupp b hb y ↔ x = y :=
 
 set_option backward.isDefEq.respectTransparency false in
 theorem ofFinsupp_def (x) : ofFinsupp b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
-  induction x using Finsupp.induction_on_max with
+  induction x using induction_on_max with
   | zero => simp
   | single_add o x f hf hx IH =>
-    rw [ofFinsupp, Finsupp.mapRange_single_add (by contrapose! hf; use o),
+    rw [ofFinsupp, mapRange_single_add (by contrapose! hf; use o),
       CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
-    · rw [Finsupp.sum_add_index' (by simp) (by simp [add_mul]), ← IH,
-        Finsupp.sum_single_index (by simp), mul_comm, ofFinsupp]
+    · rw [sum_add_index' (by simp) (by simp [add_mul]), ← IH, sum_single_index (by simp), mul_comm]
+      rfl
     · simp
     · apply CNF.eval_lt
       · simp
@@ -149,11 +149,11 @@ def toFinsuppIso : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :
     right_inv := ofFinsupp_toFinsupp b hb
     map_add' x y := by
       simp_rw [ofFinsupp_def]
-      apply Finsupp.sum_add_index'
+      apply sum_add_index'
       · simp
       · simp [add_mul]
     map_smul' := by
-      simp [ofFinsupp_def, Finsupp.sum_smul_index, Finsupp.smul_sum, Subfield.smul_def, mul_assoc]
+      simp [ofFinsupp_def, sum_smul_index, smul_sum, Subfield.smul_def, mul_assoc]
   }
 
 @[simp]

From 86bebb86d41980acf3d075cba29fc4fa372218f2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Fri, 6 Mar 2026 05:05:00 -0600
Subject: [PATCH 10/12] Update CombinatorialGames/Nimber/Finsupp.lean

---
 CombinatorialGames/Nimber/Finsupp.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CombinatorialGames/Nimber/Finsupp.lean b/CombinatorialGames/Nimber/Finsupp.lean
index f22adb0e..3dae12d7 100644
--- a/CombinatorialGames/Nimber/Finsupp.lean
+++ b/CombinatorialGames/Nimber/Finsupp.lean
@@ -163,7 +163,6 @@ theorem toFinsupp_add (x y) : toFinsupp b hb (x + y) = toFinsupp b hb x + toFins
 @[simp]
 theorem ofFinsupp_add (x y) : ofFinsupp b hb (x + y) = ofFinsupp b hb x + ofFinsupp b hb y :=
   (toFinsuppIso b hb).symm.map_add x y
-
 /-- Ordinal powers of `b` form a basis for `Nimber`. -/
 @[expose, simps!]
 def IsField.opow_basis : Module.Basis Ordinal.{u} hb.toSubfield Nimber where

From f218c41502ef3cd11a99c90c2c0ca20fc80617ae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez=20Palacios?= <vi.hdz.p@gmail.com>
Date: Sun, 8 Mar 2026 10:22:55 -0600
Subject: [PATCH 11/12] Update CombinatorialGames/Nimber/Finsupp.lean

---
 CombinatorialGames/Nimber/Finsupp.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CombinatorialGames/Nimber/Finsupp.lean b/CombinatorialGames/Nimber/Finsupp.lean
index 3dae12d7..f22adb0e 100644
--- a/CombinatorialGames/Nimber/Finsupp.lean
+++ b/CombinatorialGames/Nimber/Finsupp.lean
@@ -163,6 +163,7 @@ theorem toFinsupp_add (x y) : toFinsupp b hb (x + y) = toFinsupp b hb x + toFins
 @[simp]
 theorem ofFinsupp_add (x y) : ofFinsupp b hb (x + y) = ofFinsupp b hb x + ofFinsupp b hb y :=
   (toFinsuppIso b hb).symm.map_add x y
+
 /-- Ordinal powers of `b` form a basis for `Nimber`. -/
 @[expose, simps!]
 def IsField.opow_basis : Module.Basis Ordinal.{u} hb.toSubfield Nimber where

From 4eaa9b8c23c51ee6987edd00bb89be45935dd3ee Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Thu, 12 Mar 2026 12:09:54 -0600
Subject: [PATCH 12/12] more theorems

---
 CombinatorialGames/Nimber/Finsupp.lean | 36 ++++++++++++++++++++------
 1 file changed, 28 insertions(+), 8 deletions(-)

diff --git a/CombinatorialGames/Nimber/Finsupp.lean b/CombinatorialGames/Nimber/Finsupp.lean
index f22adb0e..17a92527 100644
--- a/CombinatorialGames/Nimber/Finsupp.lean
+++ b/CombinatorialGames/Nimber/Finsupp.lean
@@ -32,6 +32,16 @@ theorem coeff_lt {b : Ordinal} (hb : 1 < b) (o e : Ordinal) : coeff b o e < b :=
   · rw [coeff_of_notMem_CNF he]
     exact hb.pos
 
+theorem support_coeff_subset {b o x : Ordinal} (hx : x < b ^ o) :
+    SetLike.coe (coeff b x).support ⊆ Set.Iio o := by
+  obtain rfl | hb := eq_zero_or_pos b
+  · have := hx.trans_le (zero_opow_le _)
+    simp_all
+  intro e
+  rw [SetLike.mem_coe, Finsupp.mem_support_iff, Set.mem_Iio]
+  contrapose!
+  exact fun he ↦ coeff_eq_zero_of_lt (hx.trans_le (opow_le_opow_right hb he))
+
 end Ordinal.CNF
 
 namespace Finsupp
@@ -52,7 +62,7 @@ public noncomputable section
 namespace Nimber
 variable (b : Nimber) (hb : IsField b)
 
-open Finsupp Ordinal
+open Finsupp Ordinal Set
 
 /-- `toFinsupp b hb x e` returns the coefficient of `b ^ e` in `x`. This is a specialization of
 `Ordinal.CNF.coeff`. -/
@@ -70,6 +80,10 @@ private theorem toFinsupp_apply (x : Nimber) (e : Ordinal) :
 theorem toFinsupp_zero : toFinsupp b hb 0 = 0 := by
   ext; simp
 
+theorem support_toFinsupp_subset {o : Ordinal} {x : Nimber} (hx : x < ∗(b.val ^ o)) :
+    SetLike.coe (toFinsupp b hb x).support ⊆ Iio o :=
+  (SetLike.coe_subset_coe.2 (support_mapRange ..)).trans (CNF.support_coeff_subset hx)
+
 /-- Add a linear combination of ordinal powers of `b` to create a nimber. This is a specialization
 of `Ordinal.CNF.eval`. -/
 @[pp_nodot]
@@ -80,6 +94,12 @@ def ofFinsupp (x : Ordinal →₀ hb.toSubfield) : Nimber :=
 theorem ofFinsupp_zero : ofFinsupp b hb 0 = 0 := by
   simp [ofFinsupp]
 
+theorem ofFinsupp_lt {o : Ordinal} {x : Ordinal →₀ hb.toSubfield}
+    (hf : SetLike.coe x.support ⊆ Iio o) : ofFinsupp b hb x < ∗(b.val ^ o) := by
+  apply CNF.eval_lt
+  · simp
+  · aesop
+
 @[simp]
 theorem toFinsupp_ofFinsupp (x) : toFinsupp b hb (ofFinsupp b hb x) = x := by
   ext e
@@ -107,14 +127,15 @@ theorem toFinsupp_inj {x y} : toFinsupp b hb x = toFinsupp b hb y ↔ x = y :=
 theorem ofFinsupp_inj {x y} : ofFinsupp b hb x = ofFinsupp b hb y ↔ x = y :=
   (ofFinsupp_injective b hb).eq_iff
 
-set_option backward.isDefEq.respectTransparency false in
-theorem ofFinsupp_def (x) : ofFinsupp b hb x = x.sum fun o y ↦ y * ∗(b.val ^ o) := by
+theorem ofFinsupp_def (x) :
+    ofFinsupp b hb x = x.linearCombination hb.toSubfield fun o ↦ ∗(val b ^ o) := by
   induction x using induction_on_max with
   | zero => simp
   | single_add o x f hf hx IH =>
     rw [ofFinsupp, mapRange_single_add (by contrapose! hf; use o),
       CNF.eval_single_add', (hb.opow o).mul_add_eq_of_lt', hb.opow_mul_eq_of_lt]
-    · rw [sum_add_index' (by simp) (by simp [add_mul]), ← IH, sum_single_index (by simp), mul_comm]
+    · dsimp [linearCombination, lsum, Subfield.smul_def] at IH ⊢
+      rw [sum_add_index' (by simp) (by simp [add_mul]), ← IH, sum_single_index (by simp), mul_comm]
       rfl
     · simp
     · apply CNF.eval_lt
@@ -124,7 +145,7 @@ theorem ofFinsupp_def (x) : ofFinsupp b hb x = x.sum fun o y ↦ y * ∗(b.val ^
 
 @[simp]
 theorem ofFinsupp_single (x y) : ofFinsupp b hb (single x y) = y * ∗(b.val ^ x) := by
-  simp [ofFinsupp_def]
+  simp [ofFinsupp_def, Subfield.smul_def]
 
 @[simp]
 theorem toFinsupp_opow_mul (o : Ordinal) {x : Nimber} (hx : x < b) :
@@ -151,9 +172,8 @@ def toFinsuppIso : Nimber ≃ₗ[hb.toSubfield] (Ordinal →₀ hb.toSubfield) :
       simp_rw [ofFinsupp_def]
       apply sum_add_index'
       · simp
-      · simp [add_mul]
-    map_smul' := by
-      simp [ofFinsupp_def, sum_smul_index, smul_sum, Subfield.smul_def, mul_assoc]
+      · simp [add_mul, Subfield.smul_def]
+    map_smul' := by simp [ofFinsupp_def]
   }
 
 @[simp]