theorem proved term proof

`magic_8_eq_2cubed`

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

formal statement (Lean)

  29theorem magic_8_eq_2cubed : (8 : ℕ) = 2 ^ 3 := by decide

Term-mode proof.

  30
  31/-- 2 = 2^1 = minimum magic. -/

From the project-wide theorem graph. These declarations reference this one in their body.

nuclearMagicCert in IndisputableMonolith.Physics.NuclearMagicNumbersFromRS decl_use