Skip to content

fix: consolidate redundant theorem tabs (closes #13) #15

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ZRTMRH merged 1 commit into from
Apr 18, 2026
Merged

fix: consolidate redundant theorem tabs (closes #13) #15

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions Game/Levels/InnerProductWorld/Level03.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -98,17 +98,17 @@ NewTactic ring
/--
The real part of a sum of complex numbers equals the sum of their real parts.
-/
TheoremDoc Complex.add_re as "Complex.add_re" in "Complex Numbers"
TheoremDoc Complex.add_re as "Complex.add_re" in "ℂ"

/--
The real part of a complex conjugate equals the real part of the original number.
-/
TheoremDoc Complex.conj_re as "Complex.conj_re" in "Complex Numbers"
TheoremDoc Complex.conj_re as "Complex.conj_re" in "ℂ"

/--
The sum of two non-negative real numbers is non-negative.
-/
TheoremDoc add_nonneg as "add_nonneg" in "Real Numbers"
TheoremDoc add_nonneg as "add_nonneg" in "ℝ"

/--
Transitivity of the less-than-or-equal relation.
Expand All @@ -118,7 +118,7 @@ TheoremDoc le_trans as "le_trans" in "Inequalities"
/--
The product of two non-negative real numbers is non-negative.
-/
TheoremDoc mul_nonneg as "mul_nonneg" in "Real Numbers"
TheoremDoc mul_nonneg as "mul_nonneg" in "ℝ"

/--
The square of a sum: (a + b)² = a² + 2ab + b².
Expand All @@ -128,7 +128,7 @@ TheoremDoc add_sq as "add_sq" in "Algebra"
/--
The square root of a positive real number is positive.
-/
TheoremDoc Real.sqrt_pos as "Real.sqrt_pos" in "Real Numbers"
TheoremDoc Real.sqrt_pos as "Real.sqrt_pos" in "ℝ"

NewTheorem norm_nonneg Left.mul_nonneg sq_eq_sq sq_eq_sq₀ mul_assoc Complex.mul_conj Complex.normSq_eq_norm_sq Complex.re_ofReal_mul Complex.add_re Complex.conj_re add_nonneg le_trans mul_nonneg add_sq Real.sqrt_pos LinearAlgebraGame.norm_nonneg_v LinearAlgebraGame.norm_sq_eq

Expand Down
6 changes: 0 additions & 6 deletions Game/Levels/LinearIndependenceSpanWorld/Level07.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -117,12 +117,6 @@ theorem shows that type casting passes through unions.
-/
TheoremDoc Finset.coe_union as "coe_union" in "Sets"

/--
`union_subset` is a proof that if `a ⊆ c` and `b ⊆ c`, then `a ∪ b ⊆ c`. This means that if you
have two sets that are subsets of the same set, their union is also a subset of that set.
-/
TheoremDoc Set.union_subset as "union_subset" in "Sets"

/--
`sum_add_distrib` is a proof that you can distribute addition over sums. This means that if
you have functions `f : A → B`, and `g : A → B`, and some set `s : Finset A`, then
Expand Down
6 changes: 6 additions & 0 deletions Game/Levels/VectorSpaceWorld/Level05.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,12 @@ Statement subspace_neg {W : Set V} (hW : isSubspace (K := K) (V := V) W) : ∀ (
exact hx

-- Add set theory theorems needed by LinearIndependenceSpanWorld
/--
`union_subset` is a proof that if `a ⊆ c` and `b ⊆ c`, then `a ∪ b ⊆ c`. This means that if you
have two sets that are subsets of the same set, their union is also a subset of that set.
-/
TheoremDoc Set.union_subset as "union_subset" in "Sets"

NewTheorem Set.union_subset Finset.subset_union_left Finset.subset_union_right

Conclusion "You have now completed Vector Space World! The theorems proven here will be very helpful
Expand Down
Loading