one_le_formalMultilinearSeries_geometric_radius

English

The radius of the geometric formal multilinear series is at least 1.

Русский

Радиус геометрической формальной многочленной серии не меньше 1.

LaTeX

$$$1 \le (\mathrm{radius}(\mathrm{formalMultilinearSeries_geometric }\mathbb{K} A))$$$

Lean4

theorem one_le_formalMultilinearSeries_geometric_radius (𝕜 : Type*) [NontriviallyNormedField 𝕜] (A : Type*)
    [NormedRing A] [NormedAlgebra 𝕜 A] : 1 ≤ (formalMultilinearSeries_geometric 𝕜 A).radius :=
  by
  convert
    formalMultilinearSeries_geometric_eq_ofScalars 𝕜 A ▸
        FormalMultilinearSeries.ofScalars_radius_ge_inv_of_tendsto A _ one_ne_zero (by simp) |>.le
  simp

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