`zeroDefectSet_reflection_invariant`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.CompletedXiSymmetry
domain: NumberTheory
line: 110 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.CompletedXiSymmetry on GitHub at line 110.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 107  simp
 108
 109/-- The functional equation preserves the realized zero-defect set. -/
 110theorem zeroDefectSet_reflection_invariant (Ξ : CompletedXiSurface) {d : ℝ}
 111    (hd : d ∈ zeroDefectSet Ξ) :
 112    d ∈ zeroDefectSet Ξ := by
 113  rcases hd with ⟨s, hs, rfl⟩
 114  exact ⟨functionalReflection s, zero_pairing_under_reflection Ξ hs,
 115    zeroDefect_invariant_under_functional_reflection s⟩
 116
 117end
 118
 119end NumberTheory
 120end IndisputableMonolith

papers checked against this theorem

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