Stream: Is there code for X?
Topic: Möbius function
Renaud Lifchitz (Oct 13 2020 at 03:02):
Is there any code available for the Möbius function and its properties (like Möbius inversion formula)?
(see https://mathworld.wolfram.com/MoebiusFunction.html & https://en.wikipedia.org/wiki/M%C3%B6bius_inversion_formula)
Bryan Gin-ge Chen (Oct 13 2020 at 04:02):
I don't believe so. @Aaron Anderson just added arithmetic functions a little over a week ago.
Aaron Anderson (Oct 13 2020 at 04:23):
I’ll do it eventually if no one else gets around to it.
Johan Commelin (Oct 13 2020 at 05:48):
@Renaud Lifchitz If you want to add it, that would be very welcome!
Renaud Lifchitz (Oct 13 2020 at 07:47):
@Johan Commelin: Would be glad to help, but I'm just beginning with Lean...
@Aaron Anderson: That would be awesome!
@Bryan Gin-ge Chen : Thanks for the pointer.
Johan Commelin (Oct 13 2020 at 07:56):
@Renaud Lifchitz We would be glad to help
Last updated: May 17 2021 at 16:26 UTC