distrib

Mathlib.Algebra.Ring.ULift

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

Lean4

instance distrib [Distrib R] : Distrib (ULift R) :=
  { add := (· + ·), mul := (· * ·), left_distrib := fun _ _ _ => (Equiv.ulift).injective (by simp [left_distrib]),
    right_distrib := fun _ _ _ => (Equiv.ulift).injective (by simp [right_distrib]) }

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

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

Разделы

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

Аффилиация

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