hasFPowerSeriesOnBall_inv_one_sub

English

For 𝕜 and 𝕝 nontrivially normed fields, with a normed algebra structure, the inverse function x ↦ (1−x)^{-1} has a power-series expansion on the ball of radius 1 around 0.

Русский

Для ненулевых нормированных полей 𝕜 и 𝕝 с нормированной алгеброй обратная функция x ↦ (1−x)^{-1} имеет разложение в ряд степенной на шаре радиуса 1 вокруг 0.

LaTeX

$$HasFPowerSeriesOnBall (fun x : A ↦ (1 - x)^{-1}) (formalMultilinearSeries_geometric 𝕜 A) 0 1$$

Lean4

theorem hasFPowerSeriesOnBall_inv_one_sub (𝕜 𝕝 : Type*) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝]
    [NormedAlgebra 𝕜 𝕝] : HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1 :=
  by
  convert hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝
  exact Ring.inverse_eq_inv'.symm

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