Lemmas about squarefreeness of natural numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
A number is squarefree when it is not divisible by any squares except the squares of units.
Main Results #
n has no factors less than
k, returns the smallest prime
p such that
p^2 ∣ n.
Returns the smallest prime factor
n such that
p^2 ∣ n, or
none if there is no
p (that is,
n is squarefree). See also
The correctness property of the return value of
n is squarefree;
some d, then
d is a minimal square factor of
A predicate representing partial progress in a proof of