theorem proved term proof

`magic_2_eq_2pow1`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  32theorem magic_2_eq_2pow1 : (2 : ℕ) = 2 ^ 1 := by decide

Term-mode proof.

  33
  34/-- All magic numbers are in the list. -/