instRightDistribClassOrderDual

Mathlib.Algebra.Order.Ring.Synonym

URI: https://scilib.ai/kg/mathlib#instRightDistribClassOrderDual

English

If R has a right distributive structure, then the order dual R^op inherits RightDistribClass from R.

Русский

Если у R есть правое дистрибутивное тождество, то на двойственном порядке R^op оно наследуется.

LaTeX

$$RightDistribClass(R^\\mathrm{op})$$

Lean4

instance [Mul R] [Add R] [h : RightDistribClass R] : RightDistribClass Rᵒᵈ :=
  h

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

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

Разделы

Аффилиация

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