analyticOrderAt_eq_zero — Mathlib

English

If the analytic order is nonzero, then the value at z0 is zero.

Русский

Если аналитический порядок не равен нулю, то f(z0) = 0.

LaTeX

$$$\text{If } \text{analyticOrderAt } f z_0 \neq 0 \text{ then } f z_0 = 0$$$

Lean4

/-- The order of an analytic function `f` at `z₀` is zero iff `f` does not vanish at `z₀`. -/
protected theorem analyticOrderAt_eq_zero (hf : AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ = 0 ↔ f z₀ ≠ 0 := by
  simp [hf, analyticOrderAt_eq_zero]

Похожие утверждения