greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

missed one in power world

Browse Source
This commit is contained in:
Kevin Buzzard
2024-01-24 17:45:50 +00:00
parent c594db1ac5
commit e2ab764f90
1 changed files with 3 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
Game/Levels/Power/L01zero_pow_zero.lean
View File

@@ -38,12 +38,13 @@ TheoremDoc MyNat.pow_zero as "pow_zero" in "^"
NewTheorem MyNat.pow_zero
TheoremDoc MyNat.zero_pow_zero as "zero_pow_zero" in "^" "
/--
Mathematicians sometimes argue that `0 ^ 0 = 0` is also
a good convention. But it is not a good convention in this
game; all the later levels come out beautifully with the
convention that `0 ^ 0 = 1`.
"
-/
TheoremDoc MyNat.zero_pow_zero as "zero_pow_zero" in "^"
/-- $0 ^ 0 = 1$ -/
Statement zero_pow_zero : (0 : ℕ) ^ 0 = 1 := by