English
For n ≠ 0, the product of primeFactorsList(n) equals n.
Русский
Для n ≠ 0 произведение элементов primeFactorsList(n) равно n.
LaTeX
$$$ \forall {n}, n \neq 0 \Rightarrow \text{List.prod}(\text{primeFactorsList}(n)) = n $$$
Lean4
theorem prod_primeFactorsList : ∀ {n}, n ≠ 0 → List.prod (primeFactorsList n) = n
| 0 => by simp
| 1 => by simp
| k + 2 => fun _ =>
let m := minFac (k + 2)
have : (k + 2) / m < (k + 2) := factors_lemma
show (primeFactorsList (k + 2)).prod = (k + 2)
by
have h₁ : (k + 2) / m ≠ 0 := fun h =>
by
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this
rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁, Nat.mul_div_cancel' (minFac_dvd _)]
