one_lt_of_lt_mul_right — Mathlib

English

Let α be a type with a multiplication and a linear order, and assume that left multiplication reflects LT. Then for all a,b in α, if a < a b, then 1 < b.

Русский

Пусть α — множество с умножением и отношением порядка, удовлетворяющее условию отражения LT при левой умножении. Тогда для всех a,b ∈ α, если a < a b, то 1 < b.

LaTeX

$$$\forall a,b \in \alpha\quad (a < a b) \Rightarrow (1 < b)$$$

Lean4

@[to_additive]
theorem one_lt_of_lt_mul_right [MulLeftReflectLT α] {a b : α} (h : a < a * b) : 1 < b :=
  lt_of_mul_lt_mul_left' (a := a) <| by simpa only [mul_one]

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