toFinsupp_singleton — Mathlib

English

The finsupp corresponding to a singleton list [x] is the same as the finsupp with a single nonzero at index 0.

Русский

Для списка-одиночки [x] соответствующее finsupp равно единичному ненулевому элементу на позиции 0.

LaTeX

$$$$ \\operatorname{toFinsupp}([x]) = \\mathsf{Finsupp}.single\\,0\\,x. $$$$

Lean4

theorem toFinsupp_singleton (x : M) [DecidablePred (getD [x] · 0 ≠ 0)] : toFinsupp [x] = Finsupp.single 0 x := by
  ext ⟨_ | i⟩ <;> simp

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