def
definition
def or abbrev
clusteringRatio
show as:
view Lean formalization →
formal statement (Lean)
84def clusteringRatio : ℝ := 1 / phi
proof body
Definition body.
85