instAddCancelCommMonoid

Mathlib.Algebra.Order.Group.Multiset

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

Lean4

instance instAddCancelCommMonoid : AddCancelCommMonoid (Multiset α)
    where
  add_comm := Multiset.add_comm
  add_assoc := Multiset.add_assoc
  zero_add := Multiset.zero_add
  add_zero := Multiset.add_zero
  add_left_cancel _ _ _ := Multiset.add_right_inj.1
  nsmul := nsmulRec

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

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

Разделы

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

Аффилиация

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