analyticOrderAt_centeredMonomial — Mathlib

English

The analytic order at z0 of the centered monomial (z − z0)^n equals n.

Русский

Порядок аналитического нуля в точке z0 мономиального вида (z − z0)^n равен n.

LaTeX

$$$analyticOrderAt\,\bigl((\lambda z. z - z_0)^n\bigr)\, z_0 = n$$$

Lean4

/-- Simplifier lemma for the order of a centered monomial -/
@[simp]
theorem analyticOrderAt_centeredMonomial {z₀ : 𝕜} {n : ℕ} : analyticOrderAt ((· - z₀) ^ n) z₀ = n :=
  by
  rw [AnalyticAt.analyticOrderAt_eq_natCast (by fun_prop)]
  exact ⟨1, by simp [Pi.one_def, analyticAt_const]⟩

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