semiring

Mathlib.Algebra.Ring.ULift

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

Lean4

instance semiring [Semiring R] : Semiring (ULift R) :=
  { ULift.addMonoidWithOne with nsmul := AddMonoid.nsmul, npow := Monoid.npow, natCast := fun n => ULift.up n, add_comm,
    left_distrib, right_distrib, zero_mul, mul_zero, mul_assoc, one_mul, mul_one,
    npow_zero := fun _ => Monoid.npow_zero _, npow_succ := fun _ _ => Monoid.npow_succ _ _ }

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

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

Разделы

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

Аффилиация

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