Skip to content

Commit

Permalink
Merge branch 'main' into draft
Browse files Browse the repository at this point in the history
  • Loading branch information
zhangtengyu0523 committed Feb 28, 2025
2 parents 11f7cfa + 6035593 commit 14a82f7
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 5 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ jobs:
run: zip game.zip * .lake/ .i18n/ -r

- name: upload compressed game folder
uses: actions/upload-artifact@v3
uses: actions/upload-artifact@v4
with:
name: build-for-server-import
path: |
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build_blueprint.yml
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ jobs:
- uses: DeterminateSystems/magic-nix-cache-action@main
- uses: DeterminateSystems/flake-checker-action@main
- name: Checkout Project
uses: actions/checkout@v3
uses: actions/checkout@v4
with:
fetch-depth: 2
lfs: true
Expand Down
2 changes: 1 addition & 1 deletion Game/Levels/World_three.lean
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
import Game.Levels.World_three.L01_injective_definition
import Game.Levels.World_three.L01_injective_defintion
import Game.Levels.World_three.L02_injective_composition
import Game.Levels.World_three.L03_surjective_definition
import Game.Levels.World_three.L04_surjective_composition
Expand Down
3 changes: 1 addition & 2 deletions RubikCubeGame/World_2.lean
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y
exact hy

-- Level 11. Intersection of subgroups is a subgroup.
example {G : Type*} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) : Subgroup G := {
example {G : Type*} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) : Subgroup G where
carrier := H₁.carrier ∩ H₂.carrier
mul_mem' := by
intro x y ⟨hx₁, hx₂⟩ ⟨hy₁, hy₂⟩
Expand All @@ -73,7 +73,6 @@ example {G : Type*} [Group G] (H₁ : Subgroup G) (H₂ : Subgroup G) : Subgroup
exact ⟨H₁.one_mem, H₂.one_mem⟩
inv_mem' := by
simp
}

def evens : Set ℕ :=
{ n | Even n }
Expand Down

0 comments on commit 14a82f7

Please sign in to comment.