fibonacci

Stream: Is there code for X?

[ghasan jaber]

i want to build a heap data structure in Lean 4 with insert and sort operations,

[ghasan jaber]

i want [fibonacci] in lean 4

[Mario Carneiro]

docs#Nat.fib

[Notification Bot]

2 messages were moved here from #maths > Semicontinuity definition for non-linear orders by Mario Carneiro.

[ghasan jaber]

i wnat with proof

[ghasan jaber]

i want [fibonacci] in lean 4 with proof

[ghasan jaber]

i want [fibonacci] in lean 4 with proof

[Rémy Degenne]

Please don't double post and please write your messages in relevant streams and topics (or create a new topic).

[Notification Bot]

3 messages were moved here from #lean4 > Type class instance error, synthesised vs inferred by Mario Carneiro.

[Mario Carneiro]

There are many theorems about Nat.fib in mathlib. You will have to be more specific about what you are looking for