nonUnitalCommRing

Mathlib.Algebra.Ring.ULift

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

Lean4

instance nonUnitalCommRing [NonUnitalCommRing R] : NonUnitalCommRing (ULift R) :=
  { zero := (0 : ULift R), add := (· + ·), mul := (· * ·), sub := Sub.sub, neg := Neg.neg, nsmul := AddMonoid.nsmul,
    zsmul := SubNegMonoid.zsmul, zero_mul, add_assoc, zero_add, add_zero, mul_zero, left_distrib, right_distrib,
    add_comm, mul_assoc, mul_comm, nsmul_zero := fun _ => AddMonoid.nsmul_zero _, neg_add_cancel,
    nsmul_succ := fun _ _ => AddMonoid.nsmul_succ _ _, sub_eq_add_neg, zsmul_zero' := SubNegMonoid.zsmul_zero',
    zsmul_succ' := SubNegMonoid.zsmul_succ', zsmul_neg' := SubNegMonoid.zsmul_neg' .. }

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

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

Разделы

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

Аффилиация

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