`Sync`

definition

show as: view math explainer →

module: IndisputableMonolith.Gap45.Beat
domain: Gap45
line: 58 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gap45.Beat on GitHub at line 58.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  55    have : 360 ≤ n := by simpa [hk] using this
  56    exact (not_le_of_gt hnlt) this
  57
  58structure Sync where
  59  beats : Nat
  60  cycles8 : beats / 8 = 45
  61  cycles45 : beats / 45 = 8
  62
  63noncomputable def canonical : Sync :=
  64  { beats := beats
  65  , cycles8 := cycles_of_8
  66  , cycles45 := cycles_of_45 }
  67
  68end Beat
  69
  70namespace TimeLag
  71
  72@[simp] lemma lag_q : (45 : ℚ) / ((8 : ℚ) * (120 : ℚ)) = (3 : ℚ) / 64 := by
  73  norm_num
  74
  75@[simp] lemma lag_r : (45 : ℝ) / ((8 : ℝ) * (120 : ℝ)) = (3 : ℝ) / 64 := by
  76  norm_num
  77
  78end TimeLag
  79
  80end Gap45
  81end IndisputableMonolith

papers checked against this theorem

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