add_assoc

Mathlib.Data.Multiset.AddSub

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

← MathLib Explorer

English

Addition of multisets is associative: (s + t) + u = s + (t + u).

Русский

Сложение мультисетов ассоциативно: (s + t) + u = s + (t + u).

LaTeX

$$$ (s + t) + u = s + (t + u) $$$

Lean4

protected theorem add_assoc (s t u : Multiset α) : s + t + u = s + (t + u) :=
  Quotient.inductionOn₃ s t u fun _ _ _ ↦ congr_arg _ <| append_assoc ..

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

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

Разделы

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

Аффилиация

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