cardFactors_eq_one_iff_prime — Mathlib

English

Ω(n) equals 1 if and only if n is a prime number.

Русский

Ω(n) = 1 эквивалентно тому, что n — простое число.

LaTeX

$$$$\Omega(n) = 1 \iff n \text{ is prime}$$$$

Lean4

@[simp]
theorem cardFactors_eq_one_iff_prime {n : ℕ} : Ω n = 1 ↔ n.Prime :=
  by
  refine ⟨fun h => ?_, fun h => List.length_eq_one_iff.2 ⟨n, primeFactorsList_prime h⟩⟩
  cases n with
  | zero => simp at h
  | succ n =>
    rcases List.length_eq_one_iff.1 h with ⟨x, hx⟩
    rw [← prod_primeFactorsList n.add_one_ne_zero, hx, List.prod_singleton]
    apply prime_of_mem_primeFactorsList
    rw [hx, List.mem_singleton]

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