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

zeroDefect_invariant_under_functional_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)

 129theorem zeroDefect_invariant_under_functional_reflection (ρ : ℂ) :
 130    zeroDefect (functionalReflection ρ) = zeroDefect ρ := by

proof body

Tactic-mode proof.

 131  calc
 132    zeroDefect (functionalReflection ρ)
 133        =
 134          Foundation.DiscretenessForcing.J_log
 135            (zeroDeviation (functionalReflection ρ)) := zeroDefect_eq_J_log _
 136    _ = Foundation.DiscretenessForcing.J_log (-zeroDeviation ρ) := by
 137          rw [zeroDeviation_functionalReflection]
 138    _ = Foundation.DiscretenessForcing.J_log (zeroDeviation ρ) := by
 139          exact Foundation.DiscretenessForcing.J_log_symmetric (zeroDeviation ρ)
 140    _ = zeroDefect ρ := (zeroDefect_eq_J_log ρ).symm
 141
 142/-- Conjugation preserves the zero-location defect. -/

used by (2)

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

depends on (9)

Lean names referenced from this declaration's body.