Skip to content

Commit 8d75115

Browse files
Geoc2022Geoc2022
committed
Clean up
1 parent e04a9dc commit 8d75115

5 files changed

Lines changed: 4 additions & 42 deletions

File tree

‎.devcontainer/Dockerfile‎

Lines changed: 0 additions & 28 deletions
This file was deleted.

‎.devcontainer/docker-compose.yml‎

Lines changed: 0 additions & 11 deletions
This file was deleted.

‎Game/Metadata.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
import GameServer
2-
-- import Mathlib.Tactic.Common
2+
import Mathlib
3+
import Mathlib.Tactic.Common
34

45
/-! Use this file to add things that should be available in all levels.
56

‎Game/MyAlgebra/PowGroup.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ lemma inv_mpow (g : G) (n : ℕ) [Group G] : (g ^ n)⁻¹ = (g⁻¹) ^ n := by
2929
rw [← inv_id]
3030
| succ n ih =>
3131
simp
32-
simp [← inv_anticomm, ih, mpow_comm_mul]
32+
simp [mpow_add, ← inv_anticomm, ih, mpow_one, mpow_comm_mul]
3333
done
3434

3535
@[simp]

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.23.0
1+
leanprover/lean4:v4.23.0

0 commit comments

Comments
 (0)