C_one — Mathlib

English

The constant Hahn series corresponding to 1 is the unit Hahn series, i.e., the series with coefficient 1 at exponent 0 and zero elsewhere.

Русский

Пусть постоянная Hahn-переменная, соответствующая 1, является тождественной серией: коэффициент 1 при показателе 0 и ноль при прочих показателях.

LaTeX

$$$ C(1) = 1 $$$

Lean4

theorem C_one : C (1 : R) = (1 : HahnSeries Γ R) :=
  C.map_one

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