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

meromorphic_phase_charge

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 meromorphic_phase_charge (w : LocalMeromorphicWitness)
 111    (r : ℝ) (hr : 0 < r) (_hrw : r < w.radius) :
 112    ∃ cpd : ContinuousPhaseData,
 113      cpd.center = w.center ∧ cpd.radius = r ∧ cpd.charge = -w.order := by

proof body

Term-mode proof.

 114  simpa using zpow_phase_charge w.center r hr w.order
 115
 116/-! ### §3. Defect sensor phase families -/
 117

used by (3)

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

depends on (7)

Lean names referenced from this declaration's body.