English
In an ordered additive group with 1, for integers num and natural numbers n, den with n>0, the inequality (num·n)·1 < (n·den)·x is equivalent to num·1 < den·x.
Русский
В упорядоченной аддитивной группе с единицей, для целого num и натурального den, при n>0, неравенство (num·n)·1 < (n·den)·x эквивалентно num·1 < den·x.
LaTeX
$$$((\\mathrm{num} \\cdot n) \\cdot 1) < ((n \\cdot \\mathrm{den}) \\cdot x) \\iff (\\mathrm{num} \\cdot 1) < (\\mathrm{den} \\cdot x).$$$
Lean4
theorem mul_smul_one_lt_iff {num : ℤ} {n den : ℕ} (hn : 0 < n) {x : M} :
(num * n) • 1 < (n * den : ℤ) • x ↔ num • 1 < den • x :=
by
rw [mul_comm num, mul_smul, mul_smul, natCast_zsmul x den]
exact
⟨fun h ↦ lt_of_smul_lt_smul_left h (Int.natCast_nonneg n), fun h ↦ zsmul_lt_zsmul_right (Int.natCast_pos.mpr hn) h⟩
