theorem proved term proof

`primorial_one`

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

formal statement (Lean)

1355theorem primorial_one : (2 : ℕ) = 2 := rfl

Term-mode proof.

1356
1357/-- primorial(2) = 2 × 3 = 6. -/