mul_le_iff_le_one_left — Mathlib

English

In a monoid with left-monotone multiplication and commutativity, b · a ≤ a is equivalent to b ≤ 1 for cancellable a.

Русский

При моноиде с левой монотонностью и коммутативностью, для сокращаемого a верно b · a ≤ a ⇔ b ≤ 1.

LaTeX

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

Lean4

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

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