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

costSpectrumValue_prime

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)

 146theorem costSpectrumValue_prime {p : ℕ} (hp : Nat.Prime p) :
 147    costSpectrumValue p = primeCost p := by

proof body

Term-mode proof.

 148  unfold costSpectrumValue
 149  rw [Nat.Prime.factorization hp]
 150  simp [Finsupp.sum_single_index]
 151
 152/-- For a prime power `p^k`, `c(p^k) = k · J(p)`. -/

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.