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

zeroDefect_invariant_under_reflection

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)

 155theorem zeroDefect_invariant_under_reflection (ρ : ℂ) :
 156    zeroDefect (criticalReflection ρ) = zeroDefect ρ := by

proof body

Tactic-mode proof.

 157  calc
 158    zeroDefect (criticalReflection ρ)
 159        =
 160          Foundation.DiscretenessForcing.J_log
 161            (zeroDeviation (criticalReflection ρ)) := zeroDefect_eq_J_log _
 162    _ = Foundation.DiscretenessForcing.J_log (-zeroDeviation ρ) := by
 163          rw [zeroDeviation_criticalReflection]
 164    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 165          exact Foundation.DiscretenessForcing.J_log_symmetric (zeroDeviation ρ)
 166    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 167
 168end
 169
 170end NumberTheory
 171end IndisputableMonolith

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.