theorem
other
other
phasePeriod_5
show as:
view Lean formalization →
formal statement (Lean)
56@[simp] theorem phasePeriod_5 : phasePeriod 5 = 325 := by native_decide