primeFactors_eq_empty — Mathlib

English

For every n, primeFactors(n) = ∅ iff n = 0 or n = 1.

Русский

Для любого n множество простых делителей равно пустому тогда и только тогда, когда n = 0 или n = 1.

LaTeX

$$$ (n.primeFactors = \\emptyset) \\iff (n = 0 \\lor n = 1) $$$

Lean4

@[simp]
theorem primeFactors_eq_empty : n.primeFactors = ∅ ↔ n = 0 ∨ n = 1 :=
  by
  constructor
  · contrapose!
    rintro hn
    obtain ⟨p, hp, hpn⟩ := exists_prime_and_dvd hn.2
    exact Nonempty.ne_empty <| ⟨_, mem_primeFactors.2 ⟨hp, hpn, hn.1⟩⟩
  · rintro (rfl | rfl) <;> simp

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