update_zero_eq_erase

Mathlib.Algebra.SkewMonoidAlgebra.Single

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.update_zero_eq_erase

English

Updating f at a by 0 yields the same element as erasing the a-th component of f.

Русский

Обновление f в позиции a на 0 даёт то же самое, что и стереть компоненту a из f.

LaTeX

$$$f.update\\ a\\ 0 = f.erase\\ a$$$

Lean4

@[simp]
theorem update_zero_eq_erase : f.update a 0 = f.erase a := by
  classical ext; simp [coeff_update_apply, coeff_erase_apply]

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

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

Разделы

Аффилиация

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