pith. machine review for the scientific record. sign in
def definition def or abbrev

cubicDeficitFunctional

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 169def cubicDeficitFunctional (n : ℕ) : DeficitAngleFunctional n :=

proof body

Definition body.

 170  { deficit := cubicDeficit
 171  , area := cubicArea
 172  , area_pos := cubicArea_nonneg
 173  }
 174
 175/-! ## §4. Hinge product at a singleton hinge -/
 176
 177/-- Area × deficit at a singleton hinge for pair `(i, j)`, on the
 178    conformal edge-length field. -/

used by (13)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.