Commit 2023-12-26 22:33 c228bcf4

View on Github →

chore: Remove superfluous lemma that uses n.factors.toFinset (#9248) I added prod_factors_toFinset_of_squarefree before primeFactors existed. I suspect it was missed during the refactor.

Estimated changes