module
module
IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion
show as:
view Lean formalization →
depends on (1)
declarations in this module (7)
-
theorem
deLaValleePoussin_trig_kernel_eq_square -
theorem
deLaValleePoussin_trig_kernel_nonneg -
structure
DeLaValleePoussinZeroFreeRegion -
def
logZeroFreeStrip_of_deLaValleePoussin -
theorem
stripZeroFreeBridge_of_deLaValleePoussin -
structure
ClassicalZeroFreeRegionAttackSurface -
def
classicalZeroFreeRegionAttackSurface