theorem other other

`magic_2_from_dimension`

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

formal statement (Lean)

  63theorem magic_2_from_dimension : (2 : ℕ) = 2 ^ 1 := by norm_num