Commit 2021-05-01 00:19 d5d22c5d
View on Github →feat(algebra/squarefree): add sq_mul_squarefree lemmas (#7282) Every positive natural number can be expressed as m^2 * n where n is square free. Used in #7274
feat(algebra/squarefree): add sq_mul_squarefree lemmas (#7282) Every positive natural number can be expressed as m^2 * n where n is square free. Used in #7274