theorem
proved
term proof
rsKernelParams_C
show as:
view Lean formalization →
formal statement (Lean)
168@[simp] theorem rsKernelParams_C (tau0 : ℝ) (h : 0 < tau0) :
169 (rsKernelParams tau0 h).C = phi ^ (-(3 : ℝ) / 2) := rfl
proof body
Term-mode proof.
170
171/-- The eight-tick C equals 49/162. -/