instNonUnitalNonAssocSemiring

Mathlib.Data.Set.Semiring

URI: https://scilib.ai/kg/mathlib#SetSemiring.instNonUnitalNonAssocSemiring

Lean4

instance : NonUnitalNonAssocSemiring (SetSemiring α) :=
  {
    (inferInstance :
      AddCommMonoid (SetSemiring
          α)) with
    mul := fun s t => (image2 (· * ·) s.down t.down).up
    zero_mul := fun _ => empty_mul
    mul_zero := fun _ => mul_empty
    left_distrib := fun _ _ _ => mul_union
    right_distrib := fun _ _ _ => union_mul }

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

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

Разделы

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

Аффилиация

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