Topic: Binet's Formula
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!
Bryan Gin-ge Chen (Apr 04 2020 at 05:12):
We don't have it as far as I know.
Donald Sebastian Leung (Apr 04 2020 at 05:13):
Thanks - that will make it a suitable Lean exercise then :smile:
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