coeff_erase_apply

Mathlib.Algebra.SkewMonoidAlgebra.Single

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

Lean4

theorem coeff_erase_apply [DecidableEq α] : (f.erase a).coeff a' = if a' = a then 0 else f.coeff a' :=
  ite_congr rfl (fun _ ↦ rfl) (fun _ ↦ rfl)

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

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

Разделы

Аффилиация

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