def
definition
def or abbrev
vbarSq_with
show as:
view Lean formalization →
formal statement (Lean)
42def vbarSq_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
proof body
Definition body.
43 max 0 ((C.vgas r) ^ 2 + ((Real.sqrt cfg.upsilonStar) * (C.vdisk r)) ^ 2 + (C.vbul r) ^ 2)
44