one_lt_of_lt_mul_left — Mathlib

English

Let α be a type with a multiplicative structure and a compatible order. If for some a, b ∈ α we have b < a·b, then a is greater than 1.

Русский

Пусть α имеет произведение и упорядочение, совместимое между собой. Если для некоторыми a, b ∈ α выполняется b < a·b, то a > 1.

LaTeX

$$$$\forall a,b \in \alpha:\; b < a\,b \Rightarrow 1 < a.$$$$

Lean4

@[to_additive]
theorem one_lt_of_lt_mul_left [MulRightReflectLT α] {a b : α} (h : b < a * b) : 1 < a :=
  lt_of_mul_lt_mul_right' (a := b) <| by simpa only [one_mul]

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