pith. machine review for the scientific record. sign in
theorem proved term proof

nine_is_D_sq

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  85theorem nine_is_D_sq : (9 : ℕ) = 3^2 := by decide

proof body

Term-mode proof.

  86
  87/-! ## Information-theoretic content. -/
  88
  89/-- The full cross-pattern matrix has 25 entries (5×5 patterns). The
  90    non-trivial off-diagonal entries (excluding J=0 row/col which is null)
  91    are 4×4 = 16. -/

depends on (6)

Lean names referenced from this declaration's body.