def definition def or abbrev

`StripZeroFreeBridge`

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

formal statement (Lean)

  69def StripZeroFreeBridge : Prop :=

Definition body.

  70  Nonempty LogZeroFreeStrip
  71
  72/-- Any strip bridge gives the corresponding zero-free conclusion. -/

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

ClassicalZeroFreeRegionAttackSurface in IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion decl_use
logZeroFreeStrip_of_deLaValleePoussin in IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion decl_use
stripZeroFreeBridge_of_deLaValleePoussin in IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion decl_use
phase5_current_state in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use
riemannZeta_ne_zero_in_log_strip in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use
StripPhase5Cert in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use

Lean names referenced from this declaration's body.

bridge in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
LogZeroFreeStrip in IndisputableMonolith.NumberTheory.StripZeroFreeRegion decl_use