Skip to content

Commit 3ee5419

Browse files
ZRTMRHclaude
andcommitted
Fix Inner Product World Level 2: Complete theorem unlock fix
- Add inner_self_eq_zero and inner_self_im_zero to NewTheorem - Use only full namespace names (LinearAlgebraGame.X) not short aliases - Fixes "inner_self_eq_zero is not available" and "inner_self_im_zero is not available" errors in regular mode - All three theorems (inner_self_nonneg, inner_self_eq_zero, inner_self_im_zero) now properly unlocked Build verified: lake build Game.Levels.InnerProductWorld.Level02 succeeds 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <noreply@anthropic.com>
1 parent a75fae1 commit 3ee5419

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Game/Levels/InnerProductWorld/Level02.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ TheoremDoc LinearAlgebraGame.norm_zero_v as "norm_zero_v" in "Inner Product"
5151

5252
NewTactic apply_fun
5353

54-
NewTheorem Real.sq_sqrt Complex.ext LinearAlgebraGame.inner_self_nonneg inner_self_nonneg
54+
NewTheorem Real.sq_sqrt Complex.ext LinearAlgebraGame.inner_self_nonneg LinearAlgebraGame.inner_self_eq_zero LinearAlgebraGame.inner_self_im_zero
5555

5656
TheoremTab "ℂ"
5757

0 commit comments

Comments
 (0)