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.
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.