toDFinsupp_single — Mathlib

English

The toDFinsupp of a singleton in Finsupp equals the corresponding singleton in DFinsupp: (Finsupp.single i m).toDFinsupp = DFinsupp.single i m.

Русский

Переобразование к DFinsupp одиночной функции в Finsupp даёт соответствующую одиночную функцию в DFinsupp.

LaTeX

$$(Finsupp.single i m).toDFinsupp = DFinsupp.single i m$$

Lean4

@[simp]
theorem toDFinsupp_single (i : ι) (m : M) : (Finsupp.single i m).toDFinsupp = DFinsupp.single i m :=
  by
  ext
  simp [Finsupp.single_apply, DFinsupp.single_apply]

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