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

primorial_product

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)

  72theorem primorial_product : G2 * G3 * G5 = 30 := by decide

proof body

Term-mode proof.

  73
  74/-- 30 is the third primorial. The primorial spectrum is RS-canonical:
  75    p₁# = 2, p₂# = 6, p₃# = 30, p₄# = 210. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.