theorem proved term proof

`primorial_five_eq`

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

formal statement (Lean)

1367theorem primorial_five_eq : (2310 : ℕ) = 2 * 3 * 5 * 7 * 11 := by native_decide

Term-mode proof.

1368
1369/-! ### More 2310-related (primorial(5)) -/
1370
1371/-- φ(2310) = 480. -/