def definition def or abbrev

`beats`

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

formal statement (Lean)

  28@[simp] def beats : Nat := Nat.lcm 8 45

Definition body.

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

p_switch_eq in IndisputableMonolith.Decision.MontyHall decl_use
spacing_ratio_pos in IndisputableMonolith.Education.PedagogyOptimalRateFromGap45 decl_use
beats in IndisputableMonolith.Gap45 decl_use
beats_eq_360 in IndisputableMonolith.Gap45 decl_use
cycles_of_45 in IndisputableMonolith.Gap45 decl_use
cycles_of_8 in IndisputableMonolith.Gap45 decl_use
delta_time_eq_3_div_64 in IndisputableMonolith.Gap45 decl_use
minimal_sync_divides in IndisputableMonolith.Gap45 decl_use
rung45_first_conflict in IndisputableMonolith.Gap45 decl_use
beats_eq_360 in IndisputableMonolith.Gap45.Beat decl_use
canonical in IndisputableMonolith.Gap45.Beat decl_use
cycles_of_45 in IndisputableMonolith.Gap45.Beat decl_use
cycles_of_8 in IndisputableMonolith.Gap45.Beat decl_use
minimal_sync_divides in IndisputableMonolith.Gap45.Beat decl_use
Sync in IndisputableMonolith.Gap45.Beat decl_use
tetStep_jcost_pos in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
of_u4 in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
access_cost_pos_of_nonzero in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use
optimal_at_minimum_is_holographic in IndisputableMonolith.Papers.GCIC.LocalCacheForcing decl_use

Lean names referenced from this declaration's body.