theorem
proved
term proof
two_pow_seven
show as:
view Lean formalization →
formal statement (Lean)
1818theorem two_pow_seven : (2 : ℕ) ^ 7 = 128 := by native_decide
proof body
Term-mode proof.
1819
1820/-- 2^8 = 256. -/