mulRightMono

Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual

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

English

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

Русский

Если в α правая монотонность умножения, то в двойственном αᵒᵈ сохраняется правая монотонность.

LaTeX

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

Lean4

@[to_additive]
instance mulRightMono [LE α] [Mul α] [c : MulRightMono α] : MulRightMono αᵒᵈ :=
  ⟨c.1.flip⟩

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

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

Разделы

Аффилиация

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