module
module
IndisputableMonolith.Gap45.Beat
show as:
view Lean formalization →
used by (1)
depends on (1)
declarations in this module (16)
-
def
requiresExperience -
lemma
gcd_8_45_eq_one -
lemma
lcm_8_45_eq_360 -
lemma
lcm_8_45_div_8 -
lemma
lcm_8_45_div_45 -
def
beats -
lemma
beats_eq_360 -
lemma
cycles_of_8 -
lemma
cycles_of_45 -
lemma
minimal_sync_divides -
lemma
minimal_sync_360_divides -
lemma
no_smaller_multiple_8_45 -
structure
Sync -
def
canonical -
lemma
lag_q -
lemma
lag_r