mul_le_mul_iff_right — Mathlib

English

Let a be cancellable with respect to right multiplication; then right-multiplication by a preserves the order on the left: b · a ≤ c · a iff b ≤ c.

Русский

Пусть a допускает правое сокращение; тогда правое умножение на a сохраняет порядок слева: b · a ≤ c · a ⇔ b ≤ c.

LaTeX

$$MulLECancellable a → (b \cdot a ≤ c \cdot a ↔ b ≤ c)$$

Lean4

@[to_additive]
protected theorem mul_le_mul_iff_right [Mul α] [i : @Std.Commutative α (· * ·)] [MulLeftMono α] {a b c : α}
    (ha : MulLECancellable a) : b * a ≤ c * a ↔ b ≤ c := by rw [i.comm b, i.comm c, ha.mul_le_mul_iff_left]

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