theorem proved term proof

`gap_45_has_factor_9`

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

formal statement (Lean)

 329theorem gap_45_has_factor_9 : 9 ∣ gap_45 := ⟨5, rfl⟩

Term-mode proof.

 330
 331/-- The sync period 360 = 8 × 45 / gcd(8,45) = 360. -/

Lean names referenced from this declaration's body.

period in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS decl_use
gap_45 in IndisputableMonolith.Foundation.DimensionForcing decl_use