structure definition def or abbrev

`DihedralAngleData`

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

formal statement (Lean)

  93structure DihedralAngleData where
  94  cosine : ℝ
  95  cosine_bound : -1 ≤ cosine ∧ cosine ≤ 1
  96

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

cos_theta in IndisputableMonolith.Geometry.DihedralAngle decl_use
cube_dihedral in IndisputableMonolith.Geometry.DihedralAngle decl_use
cube_dihedral_theta in IndisputableMonolith.Geometry.DihedralAngle decl_use
deficit in IndisputableMonolith.Geometry.DihedralAngle decl_use
deficit_eq_zero_of_flat in IndisputableMonolith.Geometry.DihedralAngle decl_use
DihedralAngleCert in IndisputableMonolith.Geometry.DihedralAngle decl_use
DihedralAngleData in IndisputableMonolith.Geometry.DihedralAngle decl_use
DihedralAngleData in IndisputableMonolith.Geometry.DihedralAngle decl_use
FlatSumCondition in IndisputableMonolith.Geometry.DihedralAngle decl_use
regular_tet_dihedral in IndisputableMonolith.Geometry.DihedralAngle decl_use
sumThetas in IndisputableMonolith.Geometry.DihedralAngle decl_use
theta_le_pi in IndisputableMonolith.Geometry.DihedralAngle decl_use
theta_nonneg in IndisputableMonolith.Geometry.DihedralAngle decl_use
SimplicialHingeData in IndisputableMonolith.Geometry.Schlaefli decl_use
dihedral_from_cosine in IndisputableMonolith.Gravity.ReggeCalculus decl_use

Lean names referenced from this declaration's body.