mathlib
d5d22c5d - feat(algebra/squarefree): add sq_mul_squarefree lemmas (#7282)
Commit
View On GitHub
Commit
4 years ago
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
Parents
b51cee2b
FAQ Terms Privacy Refunds Impressum
Loading