def definition def or abbrev

`gapLCM`

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

formal statement (Lean)

  69def gapLCM : ℕ := Nat.lcm bodyPeriod gapPeriod

Definition body.

  70
  71/-- The arithmetic beat between the two periods, `45 - 8 = 37`. -/

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

gapLCM_eq in IndisputableMonolith.Gap45.ShimmerFactor decl_use
shimmer_cert in IndisputableMonolith.Gap45.ShimmerFactor decl_use
shimmerFactor in IndisputableMonolith.Gap45.ShimmerFactor decl_use
shimmerFactor_eq_360_div_37 in IndisputableMonolith.Gap45.ShimmerFactor decl_use
shimmer_is_gap45_arithmetic in IndisputableMonolith.Gap45.ShimmerFactor decl_use

Lean names referenced from this declaration's body.