Commit 2023-08-18 07:22 28fda0d6
View on Github →feat(Data/Nat/Squarefree): Add lemmas about the product of distinct factors of a squarefree Nat (#6344)
These lemmas will be used to develop a basic theory of arithmetic functions $n \mapsto \prod_{p\mid n} f(p)$.