nothing of importance

server/testgame/TestGame.lean

@@ -4,7 +4,7 @@ import TestGame.Levels.Proposition
 import TestGame.Levels.Implication
 import TestGame.Levels.Predicate
 import TestGame.Levels.Contradiction
-import TestGame.Levels.Prime
+-- import TestGame.Levels.Prime
 import TestGame.Levels.Sum
 -- import TestGame.Levels.Induction
 
@@ -31,7 +31,7 @@ Conclusion
 
 Path Proposition → Implication → Predicate → Predicate → Contradiction → Sum → Lean
 Path Predicate → Inequality → Sum
--- Path Predicate → Prime -- → Induction
+-- Path Inequality → Prime
 -- Path Sum → Inequality -- → Induction
 
 Path Lean → SetTheory → SetTheory2 → SetFunction

server/testgame/TestGame/Levels/Prime/L04_Prime.lean

@@ -1,46 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Data.Nat.Prime
-
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-import Mathlib.Tactic.Contrapose
-import Mathlib.Tactic.Use
-import Mathlib.Tactic.Ring
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Prime"
-Level 2
-
-Title "Primzahlen"
-
-Introduction
-"
-Eine Primzahl wird mit `(n : ℕ) (h : Nat.Prime n)` dargestellt.
-
-Wichtige Lemmas über Primzhalen werden mit
-
-```
-import Data.Nat.Prime
-```
-importiert (siehe
-[Docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html)).
-
-Insbesondere `Nat.prime_def_lt''` welches die aus der Schule bekannte Definition einer
-Primzahl `Prime p ↔ 2 ≤ p ∧ (∀ m, m ∣ p → m = 1 ∨ m = p)` gibt.
-
-Beachte: In Lean gibt es auch noch den Ausdruck `Prime n`, der beschreibt generelle
-Primelemente in einem generellen Ring. Wenn man mit natürlichen
-Zahlen arbeitet, ist es besser `Nat.Prime` zu verwenden, obwohl man natürlich zeigen kann
-dass die beiden äquivalent sind.
-"
-
-Statement
-"Zeige dass die einzigen Teiler einer Primzahl $1$ und $p$ sind."
-    (p : ℕ) (h : Nat.Prime p) : ∀ (x : ℕ), (x ∣ p) → x = 1 ∨ x = p := by
-  rw [Nat.prime_def_lt''] at h
-  rcases h with ⟨_, h₂⟩
-  assumption
-
-NewLemma Nat.prime_def_lt''

server/testgame/TestGame/Levels/Prime/L05_Prime.lean

@@ -1,42 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Data.Nat.Prime
-
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-import Mathlib.Tactic.Contrapose
-import Mathlib.Tactic.Use
-import Mathlib.Tactic.Ring
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Prime"
-Level 3
-
-Title "Primzahlen"
-
-Introduction
-"
-Mathematisch gesehen, bedeutet die Definition von vorhin dass $p$ ein
-irreduzibles Element ist, und Primzahlen sind oft durch
-`∀ (a b : ℕ), p ∣ a * b → p ∣ a ∨ p ∣ b`
-definiert. Auf den natürlichen Zahlen, sind die beiden äquivalent.
-"
-
-Statement
-"Zeige dass $p \\ge 2$ eine Primzahl ist, genau dann wenn
-$p \\mid a\\cdot b \\Rightarrow (p \\mid a) \\lor (p \\mid b)$."
-    (p : ℕ) (h₂ : 2 ≤ p):
-    Nat.Prime p ↔ ∀ (a b : ℕ), p ∣ a * b → p ∣ a ∨ p ∣ b := by
-  constructor
-  intro h a b
-  apply (Nat.Prime.dvd_mul h).mp
-  intro h
-  rw [Nat.prime_iff]
-  change p ≠ 0 ∧ ¬IsUnit p ∧ ∀ a b, p ∣ a * b → p ∣ a ∨ p ∣ b
-  rw [Nat.isUnit_iff, ←and_assoc]
-  constructor
-  constructor
-  linarith
-  linarith
-  assumption