mulLeftStrictMono

Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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