module module

`IndisputableMonolith.Geometry.DihedralCayleyMenger`

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

used by (5)

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

IndisputableMonolith.Geometry.CofactorDerivatives module_import
IndisputableMonolith.Geometry.CofactorPolynomial module_import
IndisputableMonolith.Geometry.DihedralCofactorFormula module_import
IndisputableMonolith.Geometry.DihedralDerivatives module_import
IndisputableMonolith.Gravity.SevenGaps.CausalSimplexWick module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerMatrix module_import
IndisputableMonolith.Geometry.DihedralAngle module_import
IndisputableMonolith.Geometry.ReggeRigorousFoundation module_import

declarations in this module (13)

def cmVertexIndex L40
def oppositeCMVertices L48
def dihedralDenom3 L58
def dihedralCos3Sq L64
def dihedralCos3 L70
def dihedralAngle3 L74
def dihedralAngleData3 L79
def RegularUnitCofactorCheck L89
theorem regularUnitCofactorCheck L98
theorem dihedralCos3_regularUnit_of_cofactorCheck L108
theorem dihedralAngle3_regularUnit_of_cofactorCheck L124
theorem dihedralCos3_regularUnit L132
theorem dihedralAngle3_regularUnit L138