`fibonacciCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.FibonacciSequenceFromRS
domain: Mathematics
line: 53 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Mathematics.FibonacciSequenceFromRS on GitHub at line 53.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  50  fib6_2cubeD : Nat.fib 6 = 2 ^ 3
  51  recurrence : Nat.fib 8 = Nat.fib 7 + Nat.fib 6
  52
  53def fibonacciCert : FibonacciCert where
  54  fib3 := fib3_eq_2
  55  fib4 := fib4_eq_3
  56  fib6 := fib6_eq_8
  57  fib6_2cubeD := fib6_eq_2cubeD
  58  recurrence := fib_recurrence_8
  59
  60end IndisputableMonolith.Mathematics.FibonacciSequenceFromRS

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.