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

regularity_chain

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)

 197theorem regularity_chain {lamP : Nat.Primes → ℝ}
 198    (h_self : EssentialSelfAdjointness lamP)
 199    (h_res : CompactResolvent lamP) :
 200    TraceClassHeatKernel lamP :=

proof body

Term-mode proof.

 201  ⟨h_self, h_res, trivial⟩
 202
 203/-! ## Master certificate -/
 204
 205/-- The structural facts established in this module. -/

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.