pith. machine review for the scientific record. sign in
theorem proved term proof

sync_prime_factorization

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 339theorem sync_prime_factorization : sync_period = 2^3 * 3^2 * 5 := by

proof body

Term-mode proof.

 340  unfold sync_period eight_tick gap_45; rfl
 341
 342/-- 360 degrees in a circle relates to SO(3). -/

depends on (7)

Lean names referenced from this declaration's body.