prime_mul_iff — Mathlib

English

Let a,b be natural numbers. Then ab is prime if and only if exactly one of a,b is equal to 1 and the other is prime.

Русский

Пусть a,b — натуральные числа. Произведение ab простое тогда и только тогда, когда ровно одно из a,b равно 1, а другое простое.

LaTeX

$$$$ \operatorname{Prime}(a b) \iff (\operatorname{Prime}(a) \wedge b = 1) \lor (\operatorname{Prime}(b) \wedge a = 1). $$$$

Lean4

theorem prime_mul_iff {a b : ℕ} : Nat.Prime (a * b) ↔ a.Prime ∧ b = 1 ∨ b.Prime ∧ a = 1 := by
  simp only [irreducible_mul_iff, ← irreducible_iff_nat_prime, Nat.isUnit_iff]

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