primeFactors_eq_natPrimeFactors — Mathlib

English

Let n be a natural number. The finite set of prime factors defined via the prime factorization in a unique factorization monoid coincides with Nat.primeFactors; i.e., for every n, primeFactors(n) = Nat.primeFactors(n).

Русский

Пусть n ∈ ℕ. Конечное множество простых делителей, получаемое через факторизацию в уникальном факторизационном моноиде, совпадает с Nat.primeFactors; то есть для любого n справедливо primeFactors(n) = Nat.primeFactors(n).

LaTeX

$$$\\forall n:\\mathbb{N}, \\mathrm{primeFactors}(n) = \\mathrm{Nat.primeFactors}(n)$$$

Lean4

theorem primeFactors_eq_natPrimeFactors : primeFactors = Nat.primeFactors :=
  by
  ext n : 1
  rw [primeFactors, Nat.factors_eq, Nat.primeFactors]
    -- this convert is necessary because of the different DecidableEq instances

  convert List.toFinset_coe _

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