English
MinSqFac(n) returns the smallest prime factor p of n with p^2 dividing n, or none if no such p exists.
Русский
MinSqFac(n) возвращает наименьший простый множитель p числа n, для которого p^2 делит n, либо none если такого p не существует.
LaTeX
$$$\\text{MinSqFac}(n)=\\text{none if } \\forall p, p^2 \\nmid n; \\text{ иначе } \\exists\\! p:\\, p\\text{ prime}, p^2|n \\land (\\\\forall q\\text{ prime}, q^2|n\\Rightarrow p\\le q)$$$
Lean4
/-- Returns the smallest prime factor `p` of `n` such that `p^2 ∣ n`, or `none` if there is no
such `p` (that is, `n` is squarefree). See also `Nat.squarefree_iff_minSqFac`. -/
def minSqFac (n : ℕ) : Option ℕ :=
if 2 ∣ n then
let n' := n / 2
if 2 ∣ n' then some 2 else minSqFacAux n' 3
else minSqFacAux n 3
