not_prime_mul

Mathlib.Data.Nat.Prime.Basic

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

English

If a ≠ 1 and b ≠ 1, then ab is not prime.

Русский

Если a ≠ 1 и b ≠ 1, то произведение ab не простое.

LaTeX

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

Lean4

theorem not_prime_mul {a b : ℕ} (a1 : a ≠ 1) (b1 : b ≠ 1) : ¬Prime (a * b) := by simp [prime_mul_iff, *]

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

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

Разделы

Аффилиация

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