minFac — Mathlib

English

MinFacAux is defined by: minFacAux(n, k) = n if n < k^2; = k if k | n; otherwise minFacAux(n, k+2).

Русский

minFacAux(n, k) задаётся по правилу: если n < k^2, тогда minFacAux(n, k) = n; если k | n, тогда minFacAux(n, k) = k; иначе minFacAux(n, k+2).

LaTeX

$$$\\\\minFacAux(n,k) = \\\\begin{cases} n, & n < k^2, \\\\ k, & k \\mid n, \\\\ \\\\minFacAux(n, k+2), & \\text{иначе}. \\\\end{cases}$$$

Lean4

/-- Returns the smallest prime factor of `n ≠ 1`. -/
def minFac (n : ℕ) : ℕ :=
  if 2 ∣ n then 2 else minFacAux n 3

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