`zeroCompositionWitness_forces_zero_defect`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ZeroCompositionInterface
domain: NumberTheory
line: 97 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.ZeroCompositionInterface on GitHub at line 97.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  94  (zeroCompositionLaw_forces_eta_zero w.law ρ).mp w.value_at_deviation
  95
  96/-- Therefore the zero-location defect must vanish there as well. -/
  97theorem zeroCompositionWitness_forces_zero_defect
  98    {ρ : ℂ} (w : ZeroCompositionWitness ρ) :
  99    zeroDefect ρ = 0 := by
 100  exact (zeroDefect_zero_iff_on_critical_line ρ).mpr
 101    (zeroCompositionWitness_forces_on_critical_line w)
 102
 103end
 104
 105end NumberTheory
 106end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.