IndisputableMonolith.Gravity.SevenGaps.WickFourOneAllHinges · Recognition explainer

used by (2)

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

IndisputableMonolith.Gravity.SevenGaps.WickHingeDataComplete module_import
IndisputableMonolith.Gravity.SevenGaps.WickThreeTwoHinges module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.WickActionComplexFirst module_import

declarations in this module (97)

theorem csqrt_ne_zero L106
theorem csqrt_mem_Q1 L114
theorem csqrt_ofReal_nonneg L155
theorem csqrt_four L163
theorem csqrt_ofReal_neg L173
theorem neg_one_div_im_pos L205
theorem mul_im_pos_of_Q1 L221
theorem zArc_im_nonneg L228
theorem continuousOn_csqrt_comp L244
theorem cmMatrixC_symm L288
theorem cmMinorC_symm L294
theorem cmCofactorC_symm L305
theorem dihedralCosSplitC_symm L311
theorem branchRegularOn_symm L317
theorem submatrix41_11 L338
theorem submatrix41_22 L345
def minor41_55C L353
theorem submatrix41_55 L363
theorem det_minor41_55C L373
def minor41_12C L381
theorem submatrix41_12 L396
theorem det_minor41_12C L404
def minor41_13C L410
theorem submatrix41_13 L425
theorem det_minor41_13C L433
def minor41_14C L439
theorem submatrix41_14 L454
theorem det_minor41_14C L462
def minor41_23C L468
theorem submatrix41_23 L483
theorem det_minor41_23C L491
def minor41_24C L497
theorem submatrix41_24 L512
theorem det_minor41_24C L520
def minor41_15C L526
theorem submatrix41_15 L539
theorem det_minor41_15C L547
def minor41_25C L553
theorem submatrix41_25 L566
theorem det_minor41_25C L574
def minor41_35C L580
theorem submatrix41_35 L593
theorem det_minor41_35C L601
def minor41_45C L607
theorem submatrix41_45 L620
theorem det_minor41_45C L628
theorem cofactor41_d1 L638
theorem cofactor41_d2 L644
theorem cofactor41_d5 L650
theorem cofactor41_12 L656
theorem cofactor41_13 L662
theorem cofactor41_14 L668
theorem cofactor41_23 L674
theorem cofactor41_24 L680
theorem cofactor41_15 L686
theorem cofactor41_25 L692
theorem cofactor41_35 L698
theorem cofactor41_45 L704
def fourOneCosPath L715
theorem fourOneCosPath_symm L718
theorem fourOneCosPath_apply_symm L722
theorem boundary_symm L727
theorem fourOneCosPath_eq_timelike L738
theorem fourOneCosPath_eq_spacelike L752
theorem branchRegular_fourOne_timelike_pair L765
theorem branchRegular_fourOne_spacelike_pair L816
theorem boundary_fourOne_timelike_pair L856
theorem boundary_fourOne_spacelike_pair L884
theorem branchRegular_pair01 L943
theorem branchRegular_pair02 L950
theorem branchRegular_pair03 L957
theorem branchRegular_pair12 L964
theorem branchRegular_pair13 L971
theorem branchRegular_pair23 L978
theorem branchRegular_pair04 L984
theorem branchRegular_pair14 L991
theorem branchRegular_pair24 L998
theorem branchRegular_pair34 L1005
theorem branchRegular_fourOne_allHinges L1018
theorem boundary_pair01 L1051

… and 17 more