mulRightStrictMono

Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual

URI: https://scilib.ai/kg/mathlib#OrderDual.mulRightStrictMono

English

If α has right-strict-monotone multiplication, then the dual αᵒᵈ has the same property.

Русский

Если в α есть строгая правая монотонность умножения, то в α^{op} она сохраняется.

LaTeX

$$MulRightStrictMono(α) ⇒ MulRightStrictMono(α^{op})$$

Lean4

@[to_additive]
instance mulRightStrictMono [LT α] [Mul α] [c : MulRightStrictMono α] : MulRightStrictMono αᵒᵈ :=
  ⟨c.1.flip⟩

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

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

Разделы

Аффилиация

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