theorem proved term proof

`twistedPrimeCostSum_zero`

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

formal statement (Lean)

 124@[simp]
 125theorem twistedPrimeCostSum_zero (chi : ℕ → ℝ) :
 126    twistedPrimeCostSum chi 0 = 0 := by

proof body

Term-mode proof.

 127  simp [twistedPrimeCostSum, Nat.not_prime_zero]
 128
 129/-- For the trivial character, the twisted prime cost sum equals the
 130    untwisted version. -/

depends on (4)

Lean names referenced from this declaration's body.

cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
twistedPrimeCostSum in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use
not_prime_zero in IndisputableMonolith.NumberTheory.Primes.Basic decl_use