constFormalMultilinearSeries_radius

English

For any vector v in F, the constant formal multilinear series associated to v has infinite radius of convergence.

Русский

Для любого вектора v в F постоянный ряд формальных многообразий имеет бесконечный радиус схождения.

LaTeX

$$$\operatorname{radius}\big((\text{constFormalMultilinearSeries}_{\mathbb{K}}(E,F,v))\big)=\infty$$$

Lean4

@[simp]
theorem constFormalMultilinearSeries_radius {v : F} : (constFormalMultilinearSeries 𝕜 E v).radius = ⊤ :=
  (constFormalMultilinearSeries 𝕜 E v).radius_eq_top_of_forall_image_add_eq_zero 1
    (by simp [constFormalMultilinearSeries])

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