primeFactors_eq_to_filter_divisors_prime

English

For any n, the set of prime factors equals the set of divisors of n that are prime.

Русский

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

LaTeX

$$$\displaystyle \text{primeFactors}(n) = \{ p \in \mathrm{divisors}(n) \mid p \text{ prime} \}. $$$

Lean4

/-- The factors of `n` are the prime divisors -/
theorem primeFactors_eq_to_filter_divisors_prime (n : ℕ) : n.primeFactors = {p ∈ divisors n | p.Prime} :=
  by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  · ext q
    simpa [hn, hn.ne', mem_primeFactorsList] using and_comm

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