zeroDefault

Mathlib.Testing.Plausible.Functions

URI: https://scilib.ai/kg/mathlib#Plausible.TotalFunction.zeroDefault

Lean4

/-- Map a total_function to one whose default value is zero so that it represents a finsupp. -/
@[simp]
def zeroDefault : TotalFunction α β → TotalFunction α β
  | .withDefault A _ => .withDefault A 0

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

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

Разделы

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

Аффилиация

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