update_eq_add_single

Mathlib.Algebra.Group.Finsupp

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

← MathLib Explorer

English

For f, a, b with f(a) = 0, then f.update a b = f + single a b.

Русский

Для f, a, b с условием f(a) = 0 выполняется f.update a b = f + single a b.

LaTeX

$$$f(a) = 0 \\Rightarrow f.update a b = f + single a b$$$

Lean4

theorem update_eq_add_single {f : ι →₀ M} {a : ι} (h : f a = 0) (b : M) : f.update a b = f + single a b := by
  rw [update_eq_erase_add_single, erase_of_notMem_support (by simpa)]

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

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

Разделы

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

Аффилиация

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