Commit 2022-05-04 07:50 6e003306

feat(algebra/squarefree): relate squarefree on naturals to factorization (#13816) Also moves nat.two_le_iff higher up the hierarchy since it's an elementary lemma and give it a more appropriate type. The lemma squarefree_iff_prime_sq_not_dvd has been deleted because it's a duplicate of a lemma which is already earlier in the same file.