module module

`IndisputableMonolith.Geometry.FreudenthalCubeTriangulation`

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 (3)

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

IndisputableMonolith.Geometry.FreudenthalTwoCubeStrip module_import
IndisputableMonolith.Geometry.PeriodicFreudenthalTorus module_import
IndisputableMonolith.Gravity.FreudenthalLengthChainEndpointCert module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.ReggeActionFirstVariation module_import

declarations in this module (16)

def freudenthalTetSqEdges L38
theorem cm3_freudenthalTetSqEdges L46
def freudenthalTet L52
def edgeVerts L62
def globalSqEdge L85
def tetVerts L108
def localEdgeOf L135
def edgeInTet L175
def freudenthalCube L215
theorem edgeInTet_iff_localEdgeOf L224
theorem local_sqEdge_eq_global L230
theorem edgeInTet_vertices L236
theorem localEdge_complete L245
def freudenthalCube_incidenceConsistent L250
def freudenthalCube_edgeSlotPartition L268
def freudenthalCube_edgeSlotBookkeeping L276