Fast Fourier Transform

Stream: new members

[Jagadish Bapanapally]

I see that in this link: https://leanprover-community.github.io/undergrad_todo.html Fast Fourier Transform has not been implemented yet. But, I also know that a couple of people have worked on it and implemented it in Lean. So, may I know why it is not available in Mathlib yet?

[Johan Commelin]

Could you please point to some existing implementations? I think the short answer to your question is: nobody has made a PR yet.

[Jagadish Bapanapally]

May I know what a PR is and how to create it?

[Johan Commelin]

https://www.youtube.com/watch?v=Bnc8w9lxe8A&pp=ygUdY3JlYXRlIGEgbWF0aGxpYiBwdWxsIHJlcXVlc3Q%3D

[Johan Commelin]

Voila, we have a video explaining the process (-;

[Jagadish Bapanapally]

Cool, Thanks!