English
MinSqFacProp(n, minSqFac(n)) asserts that either minSqFac(n) does not exist and n is squarefree, or if it exists, it is prime, divides n via its square, and is minimal among such primes.
Русский
MinSqFacProp(n, minSqFac(n)) утверждает, что либо minSqFac(n) не существует и n квадратносвободно, либо если существует, оно простое и p^2|n, и минимально среди таких p.
LaTeX
$$$MinSqFacProp(n, minSqFac(n)) = \\begin{cases}Squarefree(n), & minSqFac(n)=\\text{none}, \\\\ (Prime(d) \\land d^2 \\mid n \\land \\forall p, Prime(p) \\land p^2 \\mid n \\rightarrow d\\le p), & minSqFac(n)=\\text{some } d.\\end{cases}$$$
Lean4
/-- The correctness property of the return value of `minSqFac`.
* If `none`, then `n` is squarefree;
* If `some d`, then `d` is a minimal square factor of `n` -/
def MinSqFacProp (n : ℕ) : Option ℕ → Prop
| none => Squarefree n
| some d => Prime d ∧ d * d ∣ n ∧ ∀ p, Prime p → p * p ∣ n → d ≤ p
