le_mul_iff_one_le_left — Mathlib

English

In a commutative setting, b · a ≤ a implies b ≤ 1, equivalently b · a ≤ a if and only if b ≤ 1.

Русский

В коммутативной настройке из b · a ≤ a следует b ≤ 1; эквивалентно b · a ≤ a ⇔ b ≤ 1.

LaTeX

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

Lean4

@[to_additive]
protected theorem le_mul_iff_one_le_left [MulOneClass α] [i : @Std.Commutative α (· * ·)] [MulLeftMono α] {a b : α}
    (ha : MulLECancellable a) : a ≤ b * a ↔ 1 ≤ b := by rw [i.comm, ha.le_mul_iff_one_le_right]

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