Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-07 11:40 69066273

View on Github →

refactor(algebra/squarefree): split out nat part to new file data/nat/squarefree (#14577) As discussed in this Zulip thread

Estimated changes

deleted def nat.min_sq_fac
deleted def nat.min_sq_fac_aux
deleted theorem nat.min_sq_fac_dvd
deleted theorem nat.min_sq_fac_has_prop
deleted theorem nat.min_sq_fac_le_of_dvd
deleted theorem nat.min_sq_fac_prime
deleted def nat.min_sq_fac_prop
deleted theorem nat.min_sq_fac_prop_div
deleted theorem nat.sq_mul_squarefree
deleted theorem nat.squarefree.ext_iff
deleted theorem nat.squarefree_mul
deleted theorem nat.squarefree_pow_iff
deleted theorem nat.squarefree_two
added def nat.min_sq_fac
added theorem nat.min_sq_fac_dvd
added theorem nat.min_sq_fac_prime
added theorem nat.sq_mul_squarefree
added theorem nat.squarefree.ext_iff
added theorem nat.squarefree_mul
added theorem nat.squarefree_pow_iff
added theorem nat.squarefree_two