theorem proved term proof

`costSpectrumValue_zero`

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

formal statement (Lean)

 140@[simp]
 141theorem costSpectrumValue_zero : costSpectrumValue 0 = 0 := by

Term-mode proof.

 142  unfold costSpectrumValue
 143  simp [Nat.factorization_zero]
 144
 145/-- For a prime `p`, `c(p) = J(p)`. -/

Lean names referenced from this declaration's body.

costSpectrumValue in IndisputableMonolith.NumberTheory.PrimeCostSpectrum decl_use