theorem proved term proof

`gap_45_factorization`

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

formal statement (Lean)

 326theorem gap_45_factorization : gap_45 = 9 * 5 := rfl

Term-mode proof.

 327
 328/-- Gap-45 has factor 9 = 3². -/

Lean names referenced from this declaration's body.