addCommMonoid

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.addCommMonoid

Lean4

instance addCommMonoid : AddCommMonoid PartENat where
  add := (· + ·)
  zero := 0
  add_comm _ _ := Part.ext' and_comm fun _ _ => add_comm _ _
  zero_add _ := Part.ext' (iff_of_eq (true_and _)) fun _ _ => zero_add _
  add_zero _ := Part.ext' (iff_of_eq (and_true _)) fun _ _ => add_zero _
  add_assoc _ _ _ := Part.ext' and_assoc fun _ _ => add_assoc _ _ _
  nsmul := nsmulRec

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

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

Разделы

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

Аффилиация

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