factors_lemma — Mathlib

English

For every k, the quotient (k+2)/minFac(k+2) is strictly less than k+2.

Русский

Для любого k дробь (k+2)/minFac(k+2) меньше, чем k+2.

LaTeX

$$$\\\\forall k \\\\in \\\\mathbb{N}, \\\\dfrac{k+2}{\\\\minFac(k+2)} < k+2$$$

Lean4

theorem factors_lemma {k} : (k + 2) / minFac (k + 2) < k + 2 :=
  div_lt_self (Nat.zero_lt_succ _)
    (minFac_prime
        (by
          apply Nat.ne_of_gt
          apply Nat.succ_lt_succ
          apply Nat.zero_lt_succ)).one_lt

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