mulRightReflectLT — Mathlib

English

If α has right-reflecting less-than with multiplication, the dual αᵒᵈ inherits the corresponding right-reflecting less-than.

Русский

Если в α есть отражение порядка слева для < справа, то в α^{op} сохраняется соответствующее свойство слева для < справа.

LaTeX

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

Lean4

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

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