pith. machine review for the scientific record. sign in
def definition def or abbrev

stripPhase7Cert

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)

 163def stripPhase7Cert : StripPhase7Cert where
 164  boundary := boundaryZeroFreeCert

proof body

Definition body.

 165  log_strip_bridge_named := trivial
 166  critical_strip_bridge_named := trivial
 167  critical_strip_implied_by_RH :=
 168    criticalStripZeroFreeBridge_of_riemannHypothesis
 169
 170end
 171
 172end StripZeroFreeRegion
 173end NumberTheory
 174end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.