Zulip Chat Archive

Stream: maths

Topic: Binet's Formula


view this post on Zulip Donald Sebastian Leung (Apr 04 2020 at 05:09):

I just did a quick search on the mathlib docs and could not seem to find Binet's formula for the Fibonacci numbers, and would like to confirm that it is indeed not in mathlib (yet). Thanks!

view this post on Zulip Bryan Gin-ge Chen (Apr 04 2020 at 05:12):

We don't have it as far as I know.

view this post on Zulip Donald Sebastian Leung (Apr 04 2020 at 05:13):

Thanks - that will make it a suitable Lean exercise then :smile:

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 10:01):

You would either have to assume your readers could handle norm_cast or define the Fibonacci sequence as real numbers


Last updated: May 06 2021 at 18:20 UTC