mulLeftMono — Mathlib

English

If α has left-monotone multiplication, then the dual order αᵒᵈ also has left-monotone multiplication.

Русский

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

LaTeX

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

Lean4

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

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