abbrev definition def or abbrev

`fib`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  70abbrev fib : ℕ → ℕ := Nat.fib

proof body

Definition body.

  71
  72/-- The fundamental Fibonacci recurrence. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

phi_pow_44_fib in IndisputableMonolith.Cosmology.EtaBPrefactorDerivation decl_use
phi_pow_fib in IndisputableMonolith.Cosmology.EtaBPrefactorDerivation decl_use
phi_pow_44_gt_1pt5e9 in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
phi_pow_44_lt_1pt6e9 in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
phi_pow_fib_succ in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
thirteen_is_fib_7 in IndisputableMonolith.CrossDomain.CardinalitySpectrum decl_use
FibonacciPhiCert in IndisputableMonolith.CrossDomain.FibonacciPhiUniversality decl_use
fib_strict_mono in IndisputableMonolith.CrossDomain.FibonacciPhiUniversality decl_use
fib_values in IndisputableMonolith.CrossDomain.FibonacciPhiUniversality decl_use
phi_pow_bounded_by_fib in IndisputableMonolith.CrossDomain.FibonacciPhiUniversality decl_use
phi_pow_fib in IndisputableMonolith.CrossDomain.FibonacciPhiUniversality decl_use
fib in IndisputableMonolith.Gap45.Derivation decl_use
fib_0 in IndisputableMonolith.Gap45.Derivation decl_use
fib_1 in IndisputableMonolith.Gap45.Derivation decl_use
fib_2 in IndisputableMonolith.Gap45.Derivation decl_use
fib_3 in IndisputableMonolith.Gap45.Derivation decl_use
fib_4 in IndisputableMonolith.Gap45.Derivation decl_use
fib_5 in IndisputableMonolith.Gap45.Derivation decl_use
fib_6 in IndisputableMonolith.Gap45.Derivation decl_use
fib_coprime_4_5 in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_5_is_5 in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_6_is_8 in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor_is_fib in IndisputableMonolith.Gap45.Derivation decl_use
gap_forced_from_eight_tick_and_fibonacci in IndisputableMonolith.Gap45.Derivation decl_use
F_12_is_fibonacci_12 in IndisputableMonolith.Gravity.GravityParameters decl_use
coherence_exponent_from_fibonacci in IndisputableMonolith.Masses.CoherenceExponent decl_use
coherence_exponent_is_fib_5 in IndisputableMonolith.Masses.CoherenceExponent decl_use
coherence_exponent_unique in IndisputableMonolith.Masses.CoherenceExponent decl_use
D_is_fib_4 in IndisputableMonolith.Masses.CoherenceExponent decl_use
fib_4_eq in IndisputableMonolith.Masses.CoherenceExponent decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

fib in IndisputableMonolith.Gap45.Derivation decl_use
fib in IndisputableMonolith.Mathematics.RamanujanBridge.ContinuedFractionPhi decl_use