lt_mul_of_one_lt_right' — Mathlib

English

If 1 < b then a < a·b for any a in a canonically ordered monoid with left-strict monotonicity.

Русский

Если 1 < b, то a < a·b для любого a в канонически упорядоченном моноиде с левой строгой монотонностью.

LaTeX

$$$ 1 < b \\rightarrow a < a \\cdot b $$$

Lean4

@[to_additive lt_add_of_pos_right]
theorem lt_mul_of_one_lt_right' [MulLeftStrictMono α] (a : α) {b : α} (h : 1 < b) : a < a * b :=
  calc
    a = a * 1 := (mul_one a).symm
    _ < a * b := mul_lt_mul_left' h a

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