lt_mul_iff_one_lt_left' — Mathlib

English

With left-strict-monotone multiplication and left-reflect LT, for any a,b ∈ α, a < b·a is equivalent to 1 < b.

Русский

При левом строго монотонном умножении и левом отражении LT: a < b·a тогда и только тогда 1 < b.

LaTeX

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

Lean4

@[to_additive (attr := simp) lt_add_iff_pos_left]
theorem lt_mul_iff_one_lt_left' [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b : α} : a < b * a ↔ 1 < b :=
  Iff.trans (by rw [one_mul]) (mul_lt_mul_iff_right a)

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