instAddTreeMapOfZeroOfDecidableEq_mathlib

Mathlib.Tactic.Linarith.Parsing

URI: https://scilib.ai/kg/mathlib#instAddTreeMapOfZeroOfDecidableEq_mathlib

Lean4

/-- We introduce a local instance allowing addition of `TreeMap`s,
removing any keys with value zero.
We don't need to prove anything about this addition, as it is only used in meta code.
-/
local instance {α β : Type*} {c : α → α → Ordering} [Add β] [Zero β] [DecidableEq β] : Add (TreeMap α β c) where
  add := fun f g => (f.mergeWith (fun _ b b' => b + b') g).filter (fun _ b => b ≠ 0)

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

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

Разделы

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

Аффилиация

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