not_prime_of_mul_eq

Mathlib.Data.Nat.Prime.Basic

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

English

If n = a·b with a ≠ 1 and b ≠ 1, then n is not prime.

Русский

Если число n раскладывается как n = a·b с a ≠ 1 и b ≠ 1, то n не является простым.

LaTeX

$$$$ (a \cdot b = n) \land (a \neq 1) \land (b \neq 1) \Rightarrow \neg \operatorname{Prime}(n). $$$$

Lean4

theorem not_prime_of_mul_eq {a b n : ℕ} (h : a * b = n) (h₁ : a ≠ 1) (h₂ : b ≠ 1) : ¬Prime n :=
  h ▸ not_prime_mul h₁ h₂

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

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

Разделы

Аффилиация

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