lt_iff_exists_mul — Mathlib

English

For a canonical ordered monoid with MulLeftStrictMono, a < b iff there exists c > 1 with b = a·c.

Русский

Для канонически упорядоченного моноида с MulLeftStrictMono: a < b эквивалентно существованию c > 1 с b = a·c.

LaTeX

$$$ a < b \\iff \\exists c > 1,\\; b = a \\cdot c $$$

Lean4

@[to_additive]
theorem lt_iff_exists_mul [MulLeftStrictMono α] : a < b ↔ ∃ c > 1, b = a * c :=
  by
  rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
  apply exists_congr
  intro c
  rw [and_comm, and_congr_left_iff, gt_iff_lt]
  rintro rfl
  constructor
  · rw [one_lt_iff_ne_one]
    apply mt
    rintro rfl
    rw [mul_one]
  · rw [← (self_le_mul_right a c).lt_iff_ne]
    apply lt_mul_of_one_lt_right'

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