erase_cons_tail_of_mem

Mathlib.Data.Multiset.AddSub

URI: https://scilib.ai/kg/mathlib#Multiset.erase_cons_tail_of_mem

Lean4

theorem erase_cons_tail_of_mem (h : a ∈ s) : (b ::ₘ s).erase a = b ::ₘ s.erase a :=
  by
  rcases eq_or_ne a b with rfl | hab
  · simp [cons_erase h]
  · exact s.erase_cons_tail hab.symm

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

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

Разделы

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

Аффилиация

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