abscissaOfAbsConv_one — Mathlib

English

The abscissa of absolute convergence for the constant sequence 1 is 1.

Русский

Абсцисса абсолютной конвергенции константной последовательности 1 равна 1.

LaTeX

$$$\operatorname{abscissaOfAbsConv}(1) = 1.$$$

Lean4

/-- The abscissa of (absolute) convergence of the constant sequence `1` is `1`. -/
theorem abscissaOfAbsConv_one : abscissaOfAbsConv 1 = 1 :=
  modOne_eq_one (χ := χ₁) ▸ absicssaOfAbsConv_eq_one one_ne_zero χ₁

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