theorem
other
other
phasePeriod_7
show as:
view Lean formalization →
formal statement (Lean)
57@[simp] theorem phasePeriod_7 : phasePeriod 7 = 1225 := by native_decide