levels

server/testgame/TestGame.lean

@@ -13,6 +13,7 @@ import TestGame.Levels.LeanStuff
 import TestGame.Levels.SetTheory
 import TestGame.Levels.Function
 import TestGame.Levels.SetFunction
+import TestGame.Levels.LinearAlgebra
 
 
 
@@ -45,5 +46,6 @@ Path Predicate → Contradiction → LeanStuff → SetTheory → SetTheory2 →
 Path Predicate → Induction → LeanStuff → Function → SetFunction
 Path SetTheory2 → Numbers
 
+Path Module → Basis → Module2
 
 MakeGame

server/testgame/TestGame/Levels/LinearAlgebra.lean

@@ -0,0 +1,35 @@
+import TestGame.Levels.LinearAlgebra.L01_Module
+import TestGame.Levels.LinearAlgebra.L02_VectorNotation
+import TestGame.Levels.LinearAlgebra.L03_VectorNotation
+import TestGame.Levels.LinearAlgebra.L04_Submodule
+import TestGame.Levels.LinearAlgebra.L05_Submodule
+import TestGame.Levels.LinearAlgebra.L06_Span
+import TestGame.Levels.LinearAlgebra.L07_Span
+import TestGame.Levels.LinearAlgebra.L08_GeneratingSet
+
+import TestGame.Levels.LinearAlgebra.M01_LinearMap
+import TestGame.Levels.LinearAlgebra.M02_LinearIndep
+import TestGame.Levels.LinearAlgebra.M04_Basis
+import TestGame.Levels.LinearAlgebra.M05_Basis
+
+import TestGame.Levels.LinearAlgebra.N01_Span
+import TestGame.Levels.LinearAlgebra.N02_Span
+import TestGame.Levels.LinearAlgebra.N03_Idempotent
+import TestGame.Levels.LinearAlgebra.N04_Idempotent
+import TestGame.Levels.LinearAlgebra.N05_Sum
+import TestGame.Levels.LinearAlgebra.N06_Sum
+import TestGame.Levels.LinearAlgebra.N07_Prod
+import TestGame.Levels.LinearAlgebra.N08_Prod
+import TestGame.Levels.LinearAlgebra.N09_Prod
+
+Game "TestGame"
+World "Module"
+Title "Vektorraum"
+
+Game "TestGame"
+World "Basis"
+Title "Lineare Abbildungen"
+
+Game "TestGame"
+World "Module2"
+Title "Mehr Vektorräume"

server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean

@@ -0,0 +1,89 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Real.Basic      -- definiert `ℝ`
+import Mathlib.Algebra.Module.Basic -- definiert `module`
+import Mathlib.Tactic.LibrarySearch
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Module"
+Level 1
+
+Title "Module"
+
+Introduction
+"
+Vektorräume sind in Lean etwas algemeiner definiert, als dies normalerweise in
+einer Einführungsvorlesung antrifft: Man definiert ein \"Modul\" (Plural: Moduln)
+über einem Ring. Ein Modul über einem Körper wird auch \"Vektorraum\" genannt.
+Konkret heisst das:
+
+Sei `R` ein Ring. Ein `R`-Modul ist eine kommutative Gruppe `(V, +)` zusammen mit
+einer Abbildung `• : R × V → V` (Skalarmultiplitation genannt), die folgende
+Eigenschaften beliebige `(r s : R)` und `(v w : V)`erfüllt:
+- `r • (v + w) = r • v + r • w`
+- `(r + s) • v = r • v + s • v`
+- `(r * s) • v = r • s • v`
+- `1 • r = r`
+- `0 • v = 0`
+- `r • 0 = 0`
+
+Bemerkungen:
+1) Über einem `[field R]` sind die letzten beiden Eigenschaften überflüssig, diese kann
+   man beweisen, wenn man Cancellation (`a₁ + x = a₂ + x → a₁ = a₂`) hat. In einem generellen
+   Ring, muss das aber nicht gegeben sein (siehe Nullteiler).
+2) Die nötigen Annahmen um ein Modul in Lean zu erhalten sind tatsächlich noch etwas lockerer,
+   so muss `R` nicht ganz ein Ring sein (nur `[semiring R]`) und
+   `V` muss nicht ganz eine kommutative Gruppe sein (nur `[add_comm_monoid V]`).
+
+
+Einen abstrakten Vektorraum definiert man wie folgt:
+`variables {R V : Type*} [field R] [add_comm_monoid V] [module R V]`
+
+Wenn man hingegen konkret zeigen will, dass ein existierendes Objekt ein Vektorraum ist,
+kann man eine einsprechende Instanz wie folgt definieren:
+
+```
+instance Q_module : Module ℚ ℝ :=
+{ smul := λa r, ↑a * r
+  smul_zero := _
+  zero_smul := _
+  one_smul := _
+  smul_add := _
+  add_smul := _
+  mul_smul := _ }
+```
+Man muss also angeben, welche Skalarmultiplikation man gerne hätte
+(`smul`. In unserem Fall sagen wir einfach, diese soll Multiplikation in `ℝ` sein.)
+und dazu jegliche Beweise, dass die Skalarmultiplikation sich mit der Ringstruktur verträgt.
+Im nachfolgenden beweisen wir die Eigenschaften einzeln.
+"
+
+Statement
+"Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
+    : Module ℚ ℝ :=
+  { smul := fun a r ↦ ↑a * r,
+    smul_zero := by
+      intro a
+      rw [smul_zero]
+    zero_smul := by
+      intro a
+      change (0 : ℚ) * a = 0
+      simp
+    one_smul := by
+      intro b
+      change (1 : ℚ) * b = b
+      rw [Rat.cast_one, one_mul]
+    smul_add := by
+      intro a x y
+      change a * (x + y) = a * x + a * y
+      rw [mul_add]
+    add_smul := by
+      intro r s x
+      change (r + s : ℚ) * x = r * x + s * x
+      rw [Rat.cast_add, add_mul]
+    mul_smul := by
+      intro x y b
+      change (x * y : ℚ) * b = x * (y * b)
+      rw [Rat.cast_mul, mul_assoc]}

server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean

@@ -0,0 +1,75 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Algebra.Module.Pi          -- definiert `Module ℚ (fin 2 → ℚ)`
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Tactic.FinCases
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Module"
+Level 2
+
+Title "Konkrete Vektorräume"
+
+Introduction
+"
+Häufig in der linearen Algebra hat man ganz einfach Vektoren über `ℚ` oder `ℝ`
+und möchte diese explizit definieren.
+
+Reele Vektorräume definiert man in Lean am besten als Funktion von einem Indexset.
+
+So ist `Fin 2` eine Menge, die nur `0` und `1` enthält
+und `ℚ²` wird als `Fin 2 → ℚ` definiert. Hier machen wir uns eine
+lokale notation dafür:
+
+```
+notation `ℚ²` := Fin 2 → ℚ
+```
+
+Das mag auf den ersten Blick etwas unintuitiv erscheinen, hat aber den Vorteil,
+dass man die ganze
+Infrastruktur für Funktionen einfach direkt für Vektoren und
+Matrizen mitgebrauchen kann.
+
+Wir können uns auch noch ein paar andere standardmässige `ℚ`-Vektorräume definieren.
+
+```
+notation \"ℚ³\" => Fin 3 → ℚ
+notation \"ℚ^(\" n \")\" => (Fin n) → ℚ
+```
+
+Die schreibweise für einen Vektor ist `![ _, _ ]`. Zu beachten ist,
+dass man bei Zahlen explizit einen Typ angeben muss, sonst denkt sich
+Lean, man arbeite über `ℕ`.
+
+Um direkt Vektoroperationen über `ℚ` auszurechnen, kann man oft
+`#eval` benützen:
+
+```
+#eval ![ (2 : ℚ), 5 ] + ![ 1/2, -7 ]
+```
+zeigt `![5/2, -2]` an.
+
+Um eine Gleichheit in einem Beweis zu verwenden, muss man andere Taktiken
+benützen.
+
+Am hilfreichsten ist die kombination `funext i, fin_cases i`, die
+Dann eine Vektorgleichung komponentenweise aufteilt.
+
+Für jede Komponente kann man dann mit `simp` und `ring` weiterkommen.
+"
+
+notation "ℚ³" => Fin 3 → ℚ
+notation "ℚ^(" n ")" => (Fin n) → ℚ
+
+Statement
+""
+    : ![ (2 : ℚ), 5 ] + ![ 1/2, -7 ] = ![5/2, -2] := by
+  funext i
+  fin_cases i <;>
+  simp <;>
+  ring
+
+NewTactics fin_cases funext

server/testgame/TestGame/Levels/LinearAlgebra/L03_VectorNotation.lean

@@ -0,0 +1,25 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Algebra.Module.Pi          -- definiert `Module ℚ (fin 2 → ℚ)`
+import Mathlib.Data.Fin.VecNotation
+import Mathlib.Tactic.FinCases
+
+Game "TestGame"
+World "Module"
+Level 3
+
+Title "Konkrete Vektorräume"
+
+Introduction
+"
+Beachte dass Skalarmultiplikation mit `•` geschrieben wird, und nicht mit `*`!
+"
+
+Statement
+""
+    : 5 • ![ (2 : ℚ), 5 ] + ![ 1, 0 ] = ![11, 25] := by
+  funext i
+  fin_cases i <;>
+  simp <;>
+  ring

server/testgame/TestGame/Levels/LinearAlgebra/L04_Submodule.lean

@@ -0,0 +1,46 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+Game "TestGame"
+World "Module"
+Level 4
+
+Title "Untervektorräume"
+
+Introduction
+"
+Sei `K` ein Körper und `V` ein `K`-Modul.
+
+```
+variable {K V : Type _} [Field K]
+variable [AddCommMonoid V] [Module K V]
+```
+
+Untermodule/Untervektorräume werden in Lean ein bisschen anders definiert als Module/Vektorräume.
+
+Grob gesagt ist `V` ein Typ (denke z.B. an eine generelle Menge)
+und `[module K V]` eine Instanz, die von Lean automatisc gefunden wird und
+sagt, dass auf `V` eine `K`-Modulstruktur existiert. Hingegen ist `submodule K V` die Menge aller
+Untermodulen
+in `V`. Deshalb definieren wir Untermodule, indem wir Elemente aus dieser Menge auswählen:
+
+```
+variable (U : Submodule K V)
+```
+
+Unter anderem hat dies den Vorteil, dass `submodule K V` eine Lattice ist, also eine `≤`-Operation
+besitzt. Auf dem Papier
+schreibt man normalerweise `U₁ ⊆ U₂` um zu sagen, dass das eine Untermodul eine Teilmenge des
+anderen ist, in Lean braucht
+man dafür immer `≤`.
+
+Ganz `V` als Untermodul von sich selbst betrachtet, schreibt man als `⊤` (`\\top`), also das
+grösste Element in dieser Lattice,
+und das Null-Untermodule `{0}` with als `⊥` geschrieben (`\\bot`), also das kleinste Element.
+"
+
+Statement
+"Jeder Untervektorraum `U ⊆ V` ist eine Teilmenge von `V`."
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (U : Submodule K V) : U ≤ ⊤ := by
+  simp only [le_top]

server/testgame/TestGame/Levels/LinearAlgebra/L05_Submodule.lean

@@ -0,0 +1,23 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+Game "TestGame"
+World "Module"
+Level 5
+
+Title "Untervektorräume"
+
+Introduction
+"
+Elemente aus einem Untervektorraum $U$ wählt man gleich aus, wie Elemente in einer Menge.
+Nämlich man nimmt ein Element `(x : V)` und sagt, dass es in `U` liegt mit `x ∈ U` (`\\in`).
+"
+
+Statement
+"TODO: Spannendere Aufgaben."
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (U : Submodule K V) :
+    ∀ (x : V), x ∈ U ∨ x ∉ U := by
+  intro x
+  rw [or_iff_not_imp_left]
+  tauto

server/testgame/TestGame/Levels/LinearAlgebra/L06_Span.lean

@@ -0,0 +1,39 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+
+Game "TestGame"
+World "Module"
+Level 6
+
+Title "Hülle"
+
+Introduction
+"
+Ein typischer Untervektorraum ist die Hülle `⟨M⟩`, oder `span`, also die Menge aller
+`K`-Linearkombinationen von Elementen aus der Menge `M`.
+
+In Lean ist dies `Submodule.span K M`.
+
+"
+
+local notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule Set Finsupp
+
+Statement mem_span_of_mem
+  "Zeige, dass $x \\in M$ auch Element von der $K$-linearen Hülle
+  \\langle M \\rangle ist."
+    {V K : Type _} [Field K] [AddCommMonoid V]
+    [Module K V] (M : Set V) {x : V} (h : x ∈ M) :
+    x ∈ span K M := by
+  rw [mem_span]
+  intro p hp
+  specialize hp h
+  assumption

server/testgame/TestGame/Levels/LinearAlgebra/L07_Span.lean

@@ -0,0 +1,48 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+import Mathlib.Tactic.LibrarySearch
+import Mathlib
+
+Game "TestGame"
+World "Module"
+Level 7
+
+Title "Hülle"
+
+Introduction
+"
+"
+
+-- notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule Set Finsupp
+
+open BigOperators -- Summen Notation
+
+-- TODO: Why is this not in Mathlib?
+lemma mem_span_of_mem {V K : Type _} [Field K] [AddCommMonoid V]
+    [Module K V] (M : Set V) {x : V} (h : x ∈ M) :
+    x ∈ span K M := by
+  rw [mem_span]
+  intro p hp
+  specialize hp h
+  assumption
+
+Statement
+  "Für $x, y \\in M$, zeige dass $x + 2y$ in der $K$-linearen Hülle $\\langle M \\rangle$ liegt."
+    {V K : Type _} [Field K] [AddCommMonoid V] [Module K V] (M : Set V) {x y : V}
+    (h₁ : x ∈ M) (h₂ : y ∈ M) :
+    x + (2 : K) • y ∈ span K M := by
+  apply add_mem
+  apply mem_span_of_mem
+  assumption
+  apply smul_mem
+  apply mem_span_of_mem
+  assumption

server/testgame/TestGame/Levels/LinearAlgebra/L08_GeneratingSet.lean

@@ -0,0 +1,43 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+
+Game "TestGame"
+World "Module"
+Level 8
+
+Title "Erzeugendensystem"
+
+Introduction
+"
+Dass eine Familie von Vektoren `M` den ganzen Vektorraum
+aufspannt, sagt man in Lean mit `⊤ ≤ span K M`. (Man könnte auch `span K M = ⊤` schreiben,
+aber per Konvention wird `≤` bevorzugt, da `x ≤ ⊤` immer gilt (siehe `le_top`))
+"
+
+-- notation "ℝ²" => Fin 2 → ℝ
+
+open Submodule Set Finsupp
+
+open BigOperators -- Summen Notation
+
+Statement
+  "Zeige, dass `![1, 0], ![1, 1]` den ganzen `ℝ`-Vektorraum `ℝ²` aufspannt."
+    : ⊤ ≤ span ℝ (Set.range ![(![1, 0] : Fin 2 → ℝ), ![1, 1]]) := by
+  --rw [top_le_span_range_iff_forall_exists_fun]
+  sorry
+  --   intro v,
+
+  --   use ![v 0 - v 1, v 1],
+  --   simp,
+  --   funext i,
+  --   fin_cases i;
+  --   simp,
+
+--NewLemmas top_le_span_range_iff_forall_exists_fun le_top

server/testgame/TestGame/Levels/LinearAlgebra/M01_LinearMap.lean

@@ -0,0 +1,91 @@
+import TestGame.Metadata
+
+import Mathlib.Data.Real.Basic           -- definiert `ℝ`
+import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ`
+import Mathlib.Tactic.FinCases
+import Mathlib.Data.Fin.VecNotation
+
+Game "TestGame"
+World "Basis"
+Level 1
+
+notation "ℝ²" => Fin 2 → ℝ
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Sei `R` ein Ring und `V W` zwei `R`-Moduln. Eine `R`-lineare Abbildung wird in Lean
+folgendermassen geschrieben: `V →ₗ[R] W` (`\\to` + `\\_l`).
+
+Man erstellt eine lineare Abbildung aus einer Funktion `f : V → W` zusammen mit den beweisen,
+dass `f` Addition und Skalarmultiplikation erhält,
+i.e. `f (x + y) = f x + f y` und `f (r • x) = r • f x`.
+
+Hier definieren wir zum Beispiel die Null-Abbildung, die einfach alles auf `0` sendet:
+
+```
+variables {R V W : Type*} [ring R] [add_comm_monoid V] [add_comm_monoid W]
+[module R V] [module R W]
+
+def my_zero_map : V →ₗ[R] W :=
+  { to_fun := λ x, 0,
+    map_add' :=
+    begin
+      intros,
+      simp,
+    end,
+    map_smul' :=
+    begin
+      intros,
+      simp,
+    end }
+```
+
+"
+
+Statement
+"
+Zeige dass die Abbildung
+
+```
+  ℝ² → ℝ²
+  (x, y) ↦ (5x + 2y, x - y)
+```
+
+`ℝ`-linear ist.
+"
+    : ℝ² →ₗ[ℝ] ℝ² :=
+  { toFun := fun v ↦ ![5 * (v 1) + 2 * (v 2), (v 1) - (v 2)]
+    map_add' := by
+      -- Wähle zwei beliebige Vektoren mit `intros` aus.
+      intro x y
+      -- Das Lemma `funext` sagt das zwei Funktionen identisch sind, wenn sie für jeden Wert ereinstimmen:
+      -- `(∀ i, f i = g i) → f = g`. Da Vektoren einfach als Funktionen von einem Indexset codiert sind,
+      -- kannst du mit `apply funext` komponentenweise rechnen.
+      funext i
+      -- Mit `fin_cases i` kannst du pro möglichem Wert von `i` ein Goal auftun. D.h. im ersten gilt dann
+      -- `i = 0`, im zweiten Goal `i = 1`.
+      fin_cases i
+      -- Dies ist der Fall `i = 0`.
+        -- Das Goal hat jetzt Terme der Form `![a, b] 0`, und du weisst was das sein sollte, nämlich
+        -- einfach der erste Komponent `a`. Die Taktik `simp` ist für solche Vereinfachungnen gedacht.
+      · simp
+        -- Einfache Rechenaufgaben hast du ja bereits gemacht.
+        -- `ring` oder `linarith` machen dies automatisch für dich.
+        ring
+      -- Und jetzt noch den Fall `i = 1`.
+      · simp
+        ring
+    map_smul' := by
+      intro r x
+      funext i
+      fin_cases i
+        -- Bemerkung: Wenn du jetzt `simp` brauchst, macht es sogar noch mehr als vorher.
+        -- Skalarmultiplikation ist einfach als komponentenweise Multiplikation definiert.
+        -- Entsprechend braucht `simp` ein Lemma `smul_eq_mul : a • b = a * b`.
+      · simp
+        ring
+      · simp
+        ring
+  }

server/testgame/TestGame/Levels/LinearAlgebra/M02_LinearIndep.lean

@@ -0,0 +1,40 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic           -- definiert `ℝ`
+import Mathlib.Algebra.Module.LinearMap -- definiert `→ₗ`
+import Mathlib.Tactic.FinCases
+import Mathlib.Data.Fin.VecNotation
+-- import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.Algebra.BigOperators.Basic -- default
+-- import Mathlib.LinearAlgebra.LinearIndependent
+
+Game "TestGame"
+World "Basis"
+Level 2
+
+Title "Lineare Unabhängigkeit"
+
+--notation "ℝ²" => Fin 2 → ℝ
+
+Introduction
+"
+"
+
+Statement
+"Zeige, dass `![1, 0], ![1, 1]` linear unabhängig über `ℝ` sind."
+    : True := by -- linearIndependent ℝ ![(![1, 0] : ℝ²), ![1, 1]] := by
+  trivial
+
+-- begin
+--   rw fintype.linear_independent_iff,
+--   intros c h,
+--   simp at h,
+--   intros i,
+--   fin_cases i,
+--   swap,
+--   { exact h.2 },
+--   { have h' := h.1,
+--     rw [h.2, add_zero] at h',
+--     exact h'}
+-- end

server/testgame/TestGame/Levels/LinearAlgebra/M04_Basis.lean

@@ -0,0 +1,19 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+Game "TestGame"
+World "Basis"
+Level 4
+
+Title "Basis"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : True := by -- Basis (Fin 2) ℝ ℝ² := by
+  trivial

server/testgame/TestGame/Levels/LinearAlgebra/M05_Basis.lean

@@ -0,0 +1,19 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+
+Game "TestGame"
+World "Basis"
+Level 5
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    : True := by
+  trivial

server/testgame/TestGame/Levels/LinearAlgebra/N01_Span.lean

@@ -0,0 +1,30 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+
+Game "TestGame"
+World "Module2"
+Level 1
+
+open Submodule
+
+-- Verpackungswahn 1a)
+Title "Verpackungswahn"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (M : Set V) :
+    span K ↑(span K M) = span K M := by
+  apply Submodule.span_eq
+  -- or : simp

server/testgame/TestGame/Levels/LinearAlgebra/N02_Span.lean

@@ -0,0 +1,45 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic            -- definiert `ℝ`
+import Mathlib.Data.Fin.VecNotation       -- Importiert Matrix/Vektor-Notation
+--import Mathlib.LinearAlgebra.FinSupp -- contains `top_le_span_range_iff_forall_exists_fun`
+import Mathlib.Tactic.FinCases
+import Mathlib.Algebra.BigOperators.Finsupp -- default?
+import Mathlib.LinearAlgebra.Span
+import Mathlib
+
+open Submodule
+
+Game "TestGame"
+World "Module2"
+Level 2
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+  (Verpackungswahn)
+If `f` is a function and `M` a subset of its domain, then
+`f '' M` or `set.image f M` is the notation for the image, which is
+usally denoted `f(M) = {y | ∃ x ∈ M, f(x) = y}` in mathematical texts.
+"
+
+-- TODO: This is blocked by
+-- https://github.com/leanprover/lean4/issues/2074
+
+set_option autoImplicit false
+-- set_option pp.all true
+
+Statement
+"" : True := by
+  sorry
+
+-- example {K V W : Type} [Field K] [AddCommMonoid V] [AddCommMonoid W]
+--     [Module K V] [Module K W] (M : Set V) (f : V →ₗ[K] W) :
+--   f '' span K M = @span K (f '' M) := by
+--   sorry
+
+-- example {K V : Type} [Field K] [AddCommMonoid V]
+--     [Module K V] (M : Set V) (f : V →ₗ[K] V) : f '' M = f '' M =  := by
+--   rfl

server/testgame/TestGame/Levels/LinearAlgebra/N03_Idempotent.lean

@@ -0,0 +1,34 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Basic
+
+Game "TestGame"
+World "Module2"
+Level 3
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    {R V : Type _} [Semiring R] [AddCommGroup V] [Module R V]
+    (p : V →ₗ[R] V) (h : p ∘ p = p) : LinearMap.ker p ⊔ LinearMap.range p = ⊤ := by
+  sorry
+  --   rw eq_top_iff,
+  -- intros v hv,
+
+  -- rw ←sub_add_cancel v (p v),
+
+  -- apply submodule.add_mem_sup,
+  -- { rw [linear_map.mem_ker],
+  --   rw [map_sub],
+  --   change p v - (p ∘ p) v = 0,  -- oder: rw [function.comp, function.funext_iff] at h,
+  --   rw h,
+  --   simp },
+  -- { simp }

server/testgame/TestGame/Levels/LinearAlgebra/N04_Idempotent.lean

@@ -0,0 +1,33 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Basic
+
+Game "TestGame"
+World "Module2"
+Level 4
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+Statement
+""
+    {R V : Type _} [Semiring R] [AddCommGroup V] [Module R V]
+    (p : V →ₗ[R] V)(h : p ∘ p = p) : LinearMap.ker p ⊓ LinearMap.range p = ⊥ := by
+  sorry
+  -- rw eq_bot_iff,
+  -- intros v hv,
+  -- rw submodule.mem_bot,
+  -- rw submodule.mem_inf at hv,
+  -- cases hv.2 with w hw,
+  -- rw ←hw,
+  -- rw ←h,
+  -- change p (p w) = _,
+  -- rw  hw,
+  -- rw ←linear_map.mem_ker,
+  -- exact hv.1,

server/testgame/TestGame/Levels/LinearAlgebra/N05_Sum.lean

@@ -0,0 +1,26 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.LinearAlgebra.Span
+
+open Submodule
+
+Game "TestGame"
+World "Module2"
+Level 5
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Die interne Summe von Untermodulen wird in Lean mit `⊔` (`\\sup`) geschrieben.
+"
+
+Statement
+"
+Zeige, dass `V₁ ⊔ V₂` tatsächlich die interne Summe `⟨V₁ ∪ V₂⟩` ist.
+"
+    {K V : Type _} [Field K] [AddCommMonoid V] [Module K V] (V₁ V₂ : Submodule K V) :
+    V₁ ⊔ V₂ = span K ( (V₁ : Set V) ∪ V₂ ) := by
+  rw [span_union]
+  simp

server/testgame/TestGame/Levels/LinearAlgebra/N06_Sum.lean

@@ -0,0 +1,25 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.LinearAlgebra.Span
+
+open Submodule
+
+Game "TestGame"
+World "Module2"
+Level 6
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Eine interne Summe über eine Familie von Untermodulen `(T : ι → submodule K V)`
+wird als `⨆ (i : ι), T i` geschrieben (`\\supr`).
+"
+
+Statement
+""
+    {K V ι : Type _} [Field K] [AddCommMonoid V] [Module K V]
+    (T : ι → Submodule K V) : (⨆ (i : ι), T i) = span K ( ⋃ i, T i) := by
+  rw [Submodule.span_unionᵢ]
+  simp

server/testgame/TestGame/Levels/LinearAlgebra/N07_Prod.lean

@@ -0,0 +1,41 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Span
+
+Game "TestGame"
+World "Module2"
+Level 7
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Die externe Summe von (Unter-) Modulen wird als `V × W` geschrieben
+Das Produkt zweier Module wird mit `×` geschrieben.
+
+Lean weiss dann automatisch, dass das Produkt wieder ein Vektorraum ist.
+-/
+example : module ℝ (ℝ × ℝ) := infer_instance
+
+/-
+Und `ℝ × ℝ` und `fin 2 → ℝ` sind natürlich Isomorph. In Praxis eignet sich
+die Funktionsschreibweise besser, deshalb verwenden wir diese als
+definition für `ℝ²`.
+
+Hier die Äquivalenz als generelle Typen:
+-/
+example : (fin 2 → ℝ) ≃ ℝ × ℝ  :=
+begin
+  apply pi_fin_two_equiv,
+end
+
+/-
+Äquivalenz als Vektorräume schreibt man als `ℝ`-lineare Äquivalenz `≃ₗ[ℝ]`.
+"
+
+Statement
+"Zeige dass das Produkt `ℝ × ℝ` und `ℝ²` isomorph sind als `ℝ`-Vektorräume."
+    : ((Fin 2) → ℝ) ≃ₗ[ℝ] ℝ × ℝ := by
+  sorry

server/testgame/TestGame/Levels/LinearAlgebra/N08_Prod.lean

@@ -0,0 +1,57 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Span
+
+universe u
+
+Game "TestGame"
+World "Module2"
+Level 8
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+Eine Familie von Vektorräumen schreibt man erst einmal als Funktion einer Indexmenge `ι`.
+-/
+
+variables {ι : Type u} {V : ι → Type u}
+
+/-
+Für einen einzelnen Vektorraum würde man jetzt Instanzen `[add_comm_monoid V] [module K V]`
+definieren. Lean-Instanzen-Manager versteht hier `∀`-Ausdrücke:
+-/
+
+variables [∀i, add_comm_monoid (V i)] [∀i, module K (V i)]
+
+/-
+Ein externes Produkt von Vektorräumen schreibt man einfach mit `\\Pi`, also `Π i, V i`.
+
+Lean kann aus den Ausdrücken oben dann automatisch herausfinden, dass `Π i, V i`
+ein `K`-Vektorraum ist:
+"
+
+Statement
+"Sei `U` ein `K`-Vektorraum und `fᵢ : U → Vᵢ` eine Familie von `K`-lineare Abbildungen
+in `K`-Vektorräume. Dann gibt es genau eine Abbildung `f : U → (Π i, V i)`, die mit
+allen kommutiert."
+    {K U : Type u} [Field K] {ι : Type u} {V : ι → Type u}
+    [∀ i, AddCommMonoid (V i)] [∀ i, Module K (V i)]
+    [AddCommMonoid U] [Module K U]
+    (f : ∀ i, U →ₗ[K] (V i)) : U →ₗ[K] (∀ i, V i) := by
+  sorry
+-- { to_fun := λv i, f i v,
+--   map_add' :=
+--   begin
+--     intros,
+--     funext,
+--     simp,
+--   end,
+--   map_smul' :=
+--   begin
+--     intros,
+--     funext,
+--     simp,
+--   end }

server/testgame/TestGame/Levels/LinearAlgebra/N09_Prod.lean

@@ -0,0 +1,78 @@
+import TestGame.Metadata
+
+import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Span
+
+Game "TestGame"
+World "Module2"
+Level 9
+
+Title "Lineare Abbildung"
+
+Introduction
+"
+
+"
+
+universe u
+
+variable {K : Type u} [Field K]
+variable {ι : Type u} {V : ι → Type u}
+variable [∀i, AddCommMonoid (V i)] [∀i, Module K (V i)]
+
+/-
+Ein externes Summe von Vektorräumen schreibt man mit `\Pi\0`, also `Π₀ i, V i`.
+Das Suffix `_₀` wird in Mathlib häufig dafür verwendet "endlichen Support" zu bezeichnen.
+
+-/
+example : Module K (Π₀ i, V i) := inferInstance
+
+variable {U : Type u} [AddCommMonoid U] [Module K U]
+
+Statement
+"" : True := by
+  sorry
+
+-- -- :(
+-- variable [decidable_eq ι]
+-- variable [Π (i : ι) (x : V i), decidable (x ≠ 0)]
+
+-- def my_sum_map (f : Π i, V i →ₗ[K] U) : (Π₀ i, V i) →ₗ[K] U :=
+-- { to_fun := λ x, x.sum (λ i, (f i)),
+--   map_add' :=
+--   begin
+--     intros,
+--     funext,
+--     sorry,
+--   end,
+--   map_smul' :=
+--   begin
+--     intros,
+--     funext,
+--     simp,
+--     sorry
+--   end }
+
+-- Statement
+-- "Sei `U` ein `K`-Vektorraum und `fᵢ : Vᵢ → U` eine Familie von `K`-lineare Abbildungen
+-- in `K`-Vektorräume. Dann gibt es genau eine Abbildung `f : (Π₀ i, V i) → U`, die mit
+-- allen kommutiert."
+--      (f : ∀ i, V i →ₗ[K] U) :
+--   ∃! (g : (Π₀ i, V i) →ₗ[K] U), (∀ i v, f i v = g (dfinsupp.single i v)) :=
+-- by
+--   let g := my_sum_map f,
+--   use g,
+--   constructor,
+--   { simp,
+--     intros,
+--     sorry },
+--   { intros g' h,
+--     apply linear_map.ext,
+--     intro x,
+--     sorry
+--     -- change (λ i, g' x i) = λ i, f i x, -- Wieso?
+--     -- funext,
+--     -- symmetry,
+--     -- apply h,
+--   }

server/testgame/TestGame/Levels/Predicate/L09_Summary.lean

@@ -45,7 +45,7 @@ Als Abschlussübung kannst du folgende Äquivalenz zeigen:
 
 Statement
     "TODO":
-    True := by
+  True := by
   trivial
 
 Conclusion ""