theorem proved term proof

`cos_theta`

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

formal statement (Lean)

  72theorem cos_theta (d : DihedralAngleData) : Real.cos d.theta = d.cosine := by

proof body

Term-mode proof.

  73  unfold DihedralAngleData.theta
  74  exact Real.cos_arccos d.cosine_lb d.cosine_ub
  75
  76/-! ## §2. Canonical values -/
  77
  78/-- A regular tetrahedron's dihedral angle has cosine `1/3`. -/

used by (1)

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

dihedralAngleCert in IndisputableMonolith.Geometry.DihedralAngle decl_use

depends on (7)

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
DihedralAngleData in IndisputableMonolith.Geometry.DihedralAngle decl_use
DihedralAngleData in IndisputableMonolith.Gravity.ReggeCalculus decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
theta in IndisputableMonolith.NumberTheory.RiemannHypothesis.BRFPlumbing decl_use