IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges · Recognition explainer

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst module_import
IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges module_import

declarations in this module (99)

def hingeEdges32C L97
theorem continuationEdgesC_physical32 L102
def hingeMatrix32C L116
theorem cmMatrixC_hingeEdges32 L139
theorem submatrix32_44 L149
theorem submatrix32_55 L157
def minor32LowerC L166
theorem submatrix32_11 L184
theorem submatrix32_22 L190
theorem submatrix32_33 L196
theorem det_minor32LowerC L206
def minor32_45C L216
theorem submatrix32_45 L231
theorem det_minor32_45C L239
def minor32_14C L245
theorem submatrix32_14 L262
theorem det_minor32_14C L270
def minor32_15C L276
theorem submatrix32_15 L293
theorem det_minor32_15C L301
def minor32_24C L307
theorem submatrix32_24 L324
theorem det_minor32_24C L332
def minor32_25C L338
theorem submatrix32_25 L355
theorem det_minor32_25C L363
def minor32_34C L369
theorem submatrix32_34 L386
theorem det_minor32_34C L394
def minor32_35C L400
theorem submatrix32_35 L417
theorem det_minor32_35C L425
def minor32_12C L431
theorem submatrix32_12 L448
theorem det_minor32_12C L456
def minor32_13C L462
theorem submatrix32_13 L479
theorem det_minor32_13C L487
def minor32_23C L493
theorem submatrix32_23 L510
theorem det_minor32_23C L518
theorem cof32_d1 L525
theorem cof32_d2 L531
theorem cof32_d3 L537
theorem cof32_d4 L543
theorem cof32_d5 L549
theorem cof32_45 L555
theorem cof32_14 L561
theorem cof32_15 L567
theorem cof32_24 L573
theorem cof32_25 L579
theorem cof32_34 L585
theorem cof32_35 L591
theorem cof32_12 L597
theorem cof32_13 L603
theorem cof32_23 L609
theorem denom32_ne L619
def threeTwoCosPath L632
theorem threeTwoCosPath_symm L635
theorem threeTwoCosPath_apply_symm L639
theorem boundary32_symm L644
theorem threeTwoCosPath_eq_spacelike L656
theorem branchRegular_threeTwo_spacelike L670
theorem boundary_threeTwo_spacelike L716
theorem threeTwoCosPath_eq_mixed L738
theorem branchRegular_threeTwo_mixed_pair L754
theorem boundary_threeTwo_mixed_pair L800
theorem threeTwoCosPath_eq_upper L894
theorem branchRegular_threeTwo_upper_pair L910
theorem boundary_threeTwo_upper_pair L959
theorem branchRegular32_pair03 L985
theorem branchRegular32_pair04 L992
theorem branchRegular32_pair13 L999
theorem branchRegular32_pair14 L1006
theorem branchRegular32_pair23 L1013
theorem branchRegular32_pair24 L1020
theorem branchRegular32_pair01 L1027
theorem branchRegular32_pair02 L1034
theorem branchRegular32_pair12 L1041
theorem boundary32_pair03 L1047

… and 19 more