mathlib3

36dd6a66 - feat(algebra/squarefree): squarefree iff no square irreducible divisors (#11544)