module module

`IndisputableMonolith.Geometry.CayleyMengerMatrix`

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

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

IndisputableMonolith.Geometry.CofactorPolynomial module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import
IndisputableMonolith.Geometry.GramCayleyMenger module_import
IndisputableMonolith.Geometry.RealisabilityCone module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerPolynomial module_import

declarations in this module (42)

def cmMatrix3 L42
def cmDet3 L66
def cmMinor3 L71
def cmCofactorSign3 L75
def cmCofactor3 L79
theorem cmMatrix3_symm L83
theorem cmDet3_eq_cm3 L90
theorem cmDet3_regular_unit L96
theorem cmDet3_rightAngle_unit L100
theorem cmDet3_contDiff L104
theorem cmMatrix3_entry_contDiff L113
theorem cmMinor3_contDiff L121
theorem cmCofactor3_contDiff L129
def regularUnitDiagMinorMatrix L141
def regularUnitOffDiagMinorMatrix L148
def regularUnitOffDiagMinorMatrix24 L154
def regularUnitOffDiagMinorMatrix23 L160
def regularUnitOffDiagMinorMatrix14 L166
def regularUnitOffDiagMinorMatrix13 L172
def regularUnitOffDiagMinorMatrix12 L178
theorem det_regularUnitDiagMinorMatrix L184
theorem det_regularUnitOffDiagMinorMatrix L191
theorem det_regularUnitOffDiagMinorMatrix24 L198
theorem det_regularUnitOffDiagMinorMatrix23 L204
theorem det_regularUnitOffDiagMinorMatrix14 L210
theorem det_regularUnitOffDiagMinorMatrix13 L216
theorem det_regularUnitOffDiagMinorMatrix12 L222
theorem regularUnit_minor_34_eq_offDiag L230
theorem regularUnit_cofactor_34 L238
theorem regularUnit_minor_24_eq_offDiag L245
theorem regularUnit_cofactor_24 L252
theorem regularUnit_minor_23_eq_offDiag L258
theorem regularUnit_cofactor_23 L265
theorem regularUnit_minor_14_eq_offDiag L272
theorem regularUnit_cofactor_14 L279
theorem regularUnit_minor_13_eq_offDiag L286
theorem regularUnit_cofactor_13 L293
theorem regularUnit_minor_12_eq_offDiag L299
theorem regularUnit_cofactor_12 L306
theorem regularUnit_diag_minor_eq_normalForm L315
theorem regularUnit_vertex_diag_cofactor L326
theorem cmDet3_scaling L335