isZeroAt_iff — Mathlib

English

Let hg map ∞ to c. Then IsZeroAt c f k is equivalent to IsZeroAtImInfty (f|[k] g).

Русский

Пусть hg переводит ∞ в c. Тогда IsZeroAt c f k эквивалентно IsZeroAtImInfty (f|[k] g).

LaTeX

$$$\mathrm{IsZeroAt}(c,f,k) \iff \mathrm{IsZeroAtImInfty}(f \lvert[k] g)$ при $g\cdot \infty = c$$$

Lean4

/-- To check that `f` is zero at `c`, it suffices for `f ∣[k] g` to be zero at `∞` for any
single `g` with `g • ∞ = c`. -/
theorem isZeroAt_iff (hg : g • ∞ = c) : IsZeroAt c f k ↔ IsZeroAtImInfty (f ∣[k] g) :=
  ⟨fun hc ↦ hc g hg, by simp [← hg, IsZeroAt.smul_iff, isZeroAt_infty_iff]⟩

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