pith. machine review for the scientific record. sign in
theorem proved term proof

zeroDefectSet_reflection_invariant

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)

 110theorem zeroDefectSet_reflection_invariant (Ξ : CompletedXiSurface) {d : ℝ}
 111    (hd : d ∈ zeroDefectSet Ξ) :
 112    d ∈ zeroDefectSet Ξ := by

proof body

Term-mode proof.

 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

depends on (5)

Lean names referenced from this declaration's body.