not_prime_iff_minFac_lt — Mathlib

English

For n with 0 < n and not prime, minFac n ≤ n / minFac n.

Русский

Для n > 0 и не простого числа minFac n ≤ n / minFac n.

LaTeX

$$$\\\\forall {n \\\\in \\\\mathbb{N}}, \\\\text{0} < n \\\\land \\\\neg \\\\mathrm{Prime}(n) \\\\Rightarrow \\\\minFac(n) \\\\le \\\\dfrac{n}{\\\\minFac(n)}.$$$

Lean4

theorem not_prime_iff_minFac_lt {n : ℕ} (n2 : 2 ≤ n) : ¬Prime n ↔ minFac n < n :=
  (not_congr <| prime_def_minFac.trans <| and_iff_right n2).trans <|
    (lt_iff_le_and_ne.trans <| and_iff_right <| minFac_le <| le_of_succ_le n2).symm

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