commMonoid

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#PosNum.commMonoid

Lean4

instance commMonoid : CommMonoid PosNum where
  mul := (· * ·)
  one := (1 : PosNum)
  npow := @npowRec PosNum ⟨1⟩ ⟨(· * ·)⟩
  mul_assoc := by transfer
  one_mul := by transfer
  mul_one := by transfer
  mul_comm := by transfer

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

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

Разделы

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

Аффилиация

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