English
primeFactorsList n lists the prime factors of n in increasing order; 0 and 1 map to the empty list; for n ≥ 2 it recurses by taking m = minFac(n) and placing m at the head.
Русский
primeFactorsList n записывает простые множители n в возрастающем порядке; 0 и 1 соответствуют пустому списку; для n ≥ 2 выбираем m = minFac(n) и помещаем m в начало списка, продолжая рекурсию на n/m.
LaTeX
$$$\text{primeFactorsList}(0) = [],\; \text{primeFactorsList}(1) = [],\; \text{primeFactorsList}(k+2) = \minFac(k+2) :: \text{primeFactorsList}\left( \frac{k+2}{\minFac(k+2)} \right)$$$
Lean4
/-- `primeFactorsList n` is the prime factorization of `n`, listed in increasing order. -/
def primeFactorsList : ℕ → List ℕ
| 0 => []
| 1 => []
| k + 2 =>
let m := minFac (k + 2)
m :: primeFactorsList ((k + 2) / m)
decreasing_by exact factors_lemma
