nonUnitalNonAssocSemiring

Mathlib.Algebra.Ring.ULift

URI: https://scilib.ai/kg/mathlib#ULift.nonUnitalNonAssocSemiring

Lean4

instance nonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), nsmul := AddMonoid.nsmul, zero_add, add_zero, zero_mul,
    mul_zero, left_distrib, right_distrib, nsmul_zero := fun _ => AddMonoid.nsmul_zero _,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _, add_assoc, add_comm }

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

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

Разделы

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

Аффилиация

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