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)

  56structure DihedralAngleData where
  57  cosine : ℝ
  58  cosine_lb : -1 ≤ cosine
  59  cosine_ub : cosine ≤ 1
  60
  61/-- The dihedral angle itself, via `arccos`. -/
  62def DihedralAngleData.theta (d : DihedralAngleData) : ℝ := Real.arccos d.cosine

proof body

Definition body.

  63
  64/-- `θ ∈ [0, π]`. -/

used by (14)

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
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
DihedralAngleData in IndisputableMonolith.Gravity.ReggeCalculus decl_use
dihedral_from_cosine in IndisputableMonolith.Gravity.ReggeCalculus decl_use

depends on (4)

Lean names referenced from this declaration's body.

via in IndisputableMonolith.Derivations.MassToLight decl_use
DihedralAngleData in IndisputableMonolith.Gravity.ReggeCalculus decl_use
DihedralAngleData in IndisputableMonolith.Gravity.ReggeCalculus decl_use
theta in IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing decl_use