exists_dvd_of_not_prime — Mathlib

English

If n ≥ 2 and n is not prime, there exists m such that m | n and m ≠ 1 and m ≠ n.

Русский

Если n ≥ 2 и n не простое, тогда существует m such that m|n и m ≠ 1 и m ≠ n.

LaTeX

$$$$ n \ge 2 \land \neg \operatorname{Prime}(n) \Rightarrow \exists m \big( m \mid n \land m \neq 1 \land m \neq n \big). $$$$

Lean4

theorem exists_dvd_of_not_prime {n : ℕ} (n2 : 2 ≤ n) (np : ¬Prime n) : ∃ m, m ∣ n ∧ m ≠ 1 ∧ m ≠ n :=
  ⟨minFac n, minFac_dvd _, ne_of_gt (minFac_prime (ne_of_gt n2)).one_lt, ne_of_lt <| (not_prime_iff_minFac_lt n2).1 np⟩

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