mathlib

5f151043 - feat(algebra/squarefree): Defines squarefreeness, proves several equivalences (#4981)

feat(algebra/squarefree): Defines squarefreeness, proves several equivalences (#4981) Defines when a monoid element is `squarefree` Proves basic lemmas to determine squarefreeness Proves squarefreeness criteria in terms of `multiplicity`, `unique_factorization_monoid.factors`, and `nat.factors`