Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC