primeFactorsList_add_two — Mathlib

English

primeFactorsList(n+2) equals minFac(n+2) :: primeFactorsList((n+2)/minFac(n+2)).

Русский

primeFactorsList(n+2) равно minFac(n+2) :: primeFactorsList((n+2)/minFac(n+2)).

LaTeX

$$$ \text{primeFactorsList}(n+2) = \minFac(n+2) :: \text{primeFactorsList}\left( \frac{n+2}{\minFac(n+2)} \right) $$$

Lean4

/-- `primeFactorsList` can be constructed inductively by extracting `minFac`, for sufficiently
large `n`. -/
theorem primeFactorsList_add_two (n : ℕ) :
    primeFactorsList (n + 2) = minFac (n + 2) :: primeFactorsList ((n + 2) / minFac (n + 2)) := by rw [primeFactorsList]

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