mathlib3

b848b5b5 - feat(algebra/squarefree): a squarefree element of a UFM divides a power iff it divides (#5037)

feat(algebra/squarefree): a squarefree element of a UFM divides a power iff it divides (#5037) Proves that if `x, y` are elements of a UFM such that `squarefree x`, then `x | y ^ n` iff `x | y`.