Commit 2023-07-01 16:09 d48aba01
View on Github →feat(NumberTheory/ArithmeticFunction): add generalisation of moebius inversion (#5445) The standard version of Moebius inversion can't be used when the equalities only hold on a subset of the natural numbers (e.g. the squarefree numbers). Add variants of all the Moebius inversion results that generalise to well-behaved subsets of the naturals. See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Moebius.20Inversion.20on.20a.20subset.20of.20.E2.84.95