factorization_eq_zero_iff' — Mathlib

English

The only numbers with empty prime factorization are 0 and 1.

Русский

Единственные числа с пустой факторизацией — 0 и 1.

LaTeX

$$$ n.factorization = 0 \iff n = 0 \lor n = 1$$$

Lean4

/-- The only numbers with empty prime factorization are `0` and `1` -/
theorem factorization_eq_zero_iff' (n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1 :=
  by
  rw [factorization_eq_primeFactorsList_multiset n]
  simp [Multiset.coe_eq_zero]

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