theorem proved term proof

`vp_one`

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

formal statement (Lean)

  54@[simp] theorem vp_one (p : ℕ) : vp p 1 = 0 := by

Term-mode proof.

  55  simp [vp]
  56
  57/-- For a prime `p`, `vp p p = 1`. -/

Lean names referenced from this declaration's body.