theorem
proved
term proof
two_pow_sixteen
show as:
view Lean formalization →
formal statement (Lean)
1803theorem two_pow_sixteen : (2 : ℕ) ^ 16 = 65536 := by native_decide
proof body
Term-mode proof.
1804
1805/-- 2^20 = 1048576. -/