toDFinsupp

Mathlib.Data.Finsupp.ToDFinsupp

URI: https://scilib.ai/kg/mathlib#Finsupp.toDFinsupp

Lean4

/-- Interpret a `Finsupp` as a homogeneous `DFinsupp`. -/
def toDFinsupp [Zero M] (f : ι →₀ M) : Π₀ _ : ι, M where
  toFun := f
  support' := Trunc.mk ⟨f.support.1, fun i => (Classical.em (f i = 0)).symm.imp_left Finsupp.mem_support_iff.mpr⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru