instRightCommutativeErase

Mathlib.Data.Multiset.AddSub

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

English

Erasing on the right is commutative: (s.erase a).erase b = (s.erase b).erase a.

Русский

Стирание справа также коммутативно: (s.erase a).erase b = (s.erase b).erase a.

LaTeX

$$((s.erase a).erase b) = ((s.erase b).erase a)$$

Lean4

instance : RightCommutative erase (α := α) :=
  ⟨erase_comm⟩

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

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

Разделы

Аффилиация

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