Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-19 03:06 b848b5b5

View on Github →

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.

Estimated changes