Binet's Formula

Stream: maths

[Donald Sebastian Leung]

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!

[Bryan Gin-ge Chen]

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

[Donald Sebastian Leung]

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

[Kevin Buzzard]

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