not_prime_of_dvd_of_ne

Mathlib.Data.Nat.Prime.Basic

URI: https://scilib.ai/kg/mathlib#Nat.not_prime_of_dvd_of_ne

English

If m | n and m ≠ 1 and m ≠ n, then n is not prime.

Русский

Если m делит n и m ≠ 1 и m ≠ n, то n не простое.

LaTeX

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

Lean4

theorem not_prime_of_dvd_of_ne {m n : ℕ} (h1 : m ∣ n) (h2 : m ≠ 1) (h3 : m ≠ n) : ¬Prime n := fun h =>
  Or.elim (h.eq_one_or_self_of_dvd m h1) h2 h3

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru