Commit 2025-08-29 02:42 7b568f2c
View on Github →feat(Algebra/Squarefree/Basic): add lemma about indexed products of squarefree elements (#29051)
This PR also adds an import to Algebra.Squarefree.Basic.
As a drive-by, I've also simplified two proofs in Data.Nat.Squarefree.
Upstreamed from formal-conjectures