Euler-Binet formula

Stream: mathlib4

[Kamila Szewczyk]

Hello, I would like to supply my proof of the Euler-Binet formula and related results (negative Fibonacci numbers, bounds on Fibonacci numbers, ratio of consecutive Fibonacci numbers) to Mathlib. May I request write access to a branch for this purpose? I am an university student (my homepage: https://palaiologos.rocks) and I am taking part in a seminar which encourages students to submit their contributions to mathlib4. My Github handle is @kspalaiologos.

[Ruben Van de Velde]

@maintainers

[Riccardo Brasca]

Invitation sent!

[Riccardo Brasca]

Are we missing Binet formula?! This is surprising

[Anatole Dedecker]

I think we have it because it was one of my first projects…

[Riccardo Brasca]

@loogle Nat.fib, Real.sqrt

[Riccardo Brasca]

@loogle Nat.fib, Real.sqrt

[loogle]

:search: Real.coe_fib_eq, Real.coe_fib_eq'

[Riccardo Brasca]

Thanks

[Anatole Dedecker]

That said we don’t have all the consequences you mention, I think

[Riccardo Brasca]

I guess that this should be mentioned in Mathlib.Data.Nat.Fib.Basic

[Kamila Szewczyk]

Whom should I assign the pull request to for review?

[Kevin Buzzard]

Nobody -- just make sure that it appears on #queue (i.e. check that it has a green tick and is tagged awaiting-review) and someone will look at it I'm sure.

[Riccardo Brasca]

Note that we are all busy with the Lean Together, so maybe nobody will review it before the weekend, but don't worry!

[Kamila Szewczyk]

That's OK, thank you!