Commit 2026-08-19 10:07 50838443
View on Github →feat(Algebra/Squarefree): add exists_sq_mul_squarefree (#42319)
Add exists_sq_mul_squarefree: every element of a unique factorization monoid is a square times a squarefree element. Also add Squarefree.dvd_of_isSquare_mul and Squarefree.associated_of_isSquare_mul, and golf the existing Nat.sq_mul_squarefree and Nat.sq_mul_squarefree_of_pos to use the new lemma.