formalMultilinearSeries_geometric_radius

English

Let 𝕜 be a nontrivial normed field and A a normed algebra with a unit. Then the radius of the geometric formal multilinear series associated to 𝕜 and A is equal to 1.

Русский

Пусть 𝕜 — ненулевое нормированное поле и A — нормированная алгебра с единицей. Тогда радиус геометрической формальной многочленной серии, связанной с 𝕜 и A, равен 1.

LaTeX

$$$\operatorname{radius}\bigl( \text{formalMultilinearSeries}_{\mathrm{geometric}}(\mathbb{k},A) \bigr) = 1$$$

Lean4

theorem formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*) [NormedRing A]
    [NormOneClass A] [NormedAlgebra 𝕜 A] : (formalMultilinearSeries_geometric 𝕜 A).radius = 1 :=
  formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
    FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto A _ one_ne_zero (by simp)

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