def definition def or abbrev

`fibonacci_factor`

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

formal statement (Lean)

 149def fibonacci_factor : ℕ := 5

Definition body.

 150
 151/-- 9 × 5 = 45. -/

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

D_3_forced_from_structure in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor_coprime_with_8 in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor_eq in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_factor_is_fib in IndisputableMonolith.Gap45.Derivation decl_use
fibonacci_interpretation in IndisputableMonolith.Gap45.Derivation decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
gap_coprime_with_8 in IndisputableMonolith.Gap45.Derivation decl_use
gap_forced_from_eight_tick_and_fibonacci in IndisputableMonolith.Gap45.Derivation decl_use
derivations_equivalent in IndisputableMonolith.Gap45.PhysicalMotivation decl_use
nine_times_five in IndisputableMonolith.Gap45.PhysicalMotivation decl_use

Lean names referenced from this declaration's body.