coe_toFinsupp — Mathlib

English

The ith value of the finsupp obtained from l coincides with the i-th entry of l, with default value 0 for out-of-range indices.

Русский

i-ое значение копии finsupp, полученной из списка l, совпадает с i-й позицией списка, а за пределами длины списка применяется значение 0.

LaTeX

$$$$ (l\\toFinsupp)(i) = \\begin{cases} l_i, & i < |l|, \\\\ 0, & i \\ge |l|. \\end{cases} $$$$

Lean4

@[norm_cast]
theorem coe_toFinsupp : (l.toFinsupp : ℕ → M) = (l.getD · 0) :=
  rfl

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