def definition def or abbrev

`totalTheta`

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

formal statement (Lean)

  92def totalTheta (h : SimplicialHingeData) : ℝ :=

Definition body.

  93  DihedralAngle.sumThetas h.dihedrals
  94
  95/-- Deficit at the hinge: `2π − Σ θ`. -/

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

LinearizationCoefficients in IndisputableMonolith.Geometry.DeficitLinearization decl_use
deficit_eq in IndisputableMonolith.Geometry.Schlaefli decl_use
schlaefli_kills_dtheta in IndisputableMonolith.Geometry.Schlaefli decl_use

Lean names referenced from this declaration's body.