minFac_le_of_dvd — Mathlib

English

If 0 < n and n is not prime, then minFac(n) ≤ n / minFac(n).

Русский

Если 0 < n и n не простое, то minFac(n) ≤ n / minFac(n).

LaTeX

$$$\\\\text{0} < n \\\\land \\\\neg \\\\mathrm{Prime}(n) \\\\Rightarrow \\\\minFac(n) \\\\le \\\\dfrac{n}{\\\\minFac(n)}.$$$

Lean4

theorem minFac_le_of_dvd {n : ℕ} : ∀ {m : ℕ}, 2 ≤ m → m ∣ n → minFac n ≤ m :=
  by
  by_cases n1 : n = 1
  · exact fun m2 _ => n1.symm ▸ le_trans (by simp) m2
  · apply (minFac_has_prop n1).2.2

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