def
definition
def or abbrev
bao_correlation_peak
show as:
view Lean formalization →
formal statement (Lean)
139noncomputable def bao_correlation_peak (r_s : ℝ) : ℝ := 2 * r_s
proof body
Definition body.
140