toMulRightMono — Mathlib

English

Multiplication on the right preserves order: if a ≤ b then a · c ≤ b · c for all c.

Русский

Умножение справа сохраняет порядок: если a ≤ b, то для всех c выполняется a · c ≤ b · c.

LaTeX

$$$\forall a,b,c \in \alpha,\ a \le b \Rightarrow a \cdot c \le b \cdot c$$$

Lean4

instance (priority := 100) toMulRightMono : MulRightMono α :=
  ⟨fun a b c hbc ↦ add_eq_left_iff_le.1 <| by rw [← add_mul, hbc.add_eq_left]⟩

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