English
The trailing coefficient of the map z ↦ z − y at x is 1 if x = y, and x − y otherwise.
Русский
Хвостовой коэффициент отображения z ↦ z − y в точке x равен 1, если x = y, иначе x − y.
LaTeX
$$$$\mathrm{meromorphicTrailingCoeffAt}(\lambda z. z - y, x) = \begin{cases} 1, & x = y \\ x - y, & x \neq y \end{cases}.$$$$
Lean4
/-- The trailing coefficient of `fun z ↦ z - constant` at `z₀` equals one if `z₀ = constant`, or else
`z₀ - constant`.
-/
theorem meromorphicTrailingCoeffAt_id_sub_const [DecidableEq 𝕜] {x y : 𝕜} :
meromorphicTrailingCoeffAt (· - y) x = if x = y then 1 else x - y :=
by
by_cases h : x = y
· simp_all only [sub_self, ite_true]
apply AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 1) (by fun_prop) (by apply one_ne_zero)
simp
· simp_all only [ite_false]
apply AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero (by fun_prop)
simp_all [sub_ne_zero]
