single_zero_natCast — Mathlib

English

For natural numbers n with at least two, the Hahn series supported at 0 with value n equals the natCast of n.

Русский

Для натурального n с условием n ≥ 2 вложение в нулевую степень даёт коэффициент, равный n как натуральное число.

LaTeX

$$$\mathrm{single}(0, \mathrm{ofNat}(n)) = \mathrm{ofNat}(n)$$$

Lean4

theorem single_zero_natCast [Zero R] [NatCast R] (n : ℕ) : single (0 : Γ) (n : R) = n :=
  rfl

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