IndisputableMonolith.Geometry.CofactorPolynomial · Recognition explainer

used by (1)

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

IndisputableMonolith.Geometry.CofactorDerivatives module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Geometry.CayleyMengerMatrix module_import
IndisputableMonolith.Geometry.DihedralCayleyMenger module_import

declarations in this module (116)

def cmCofactor3Poly L27
def cmCofactorPartial L58
def CofactorPolynomialAgreement L204
def cmMinor34Matrix L210
theorem cmMinor34_submatrix_eq L218
theorem det_cmMinor34Matrix L225
theorem cmCofactor3_34_eq_poly L232
def cmMinor24Matrix L240
theorem cmMinor24_submatrix_eq L246
theorem det_cmMinor24Matrix L252
theorem cmCofactor3_24_eq_poly L258
def cmMinor23Matrix L265
theorem cmMinor23_submatrix_eq L271
theorem det_cmMinor23Matrix L277
theorem cmCofactor3_23_eq_poly L283
def cmMinor14Matrix L290
theorem cmMinor14_submatrix_eq L296
theorem det_cmMinor14Matrix L302
theorem cmCofactor3_14_eq_poly L308
def cmMinor13Matrix L315
theorem cmMinor13_submatrix_eq L321
theorem det_cmMinor13Matrix L327
theorem cmCofactor3_13_eq_poly L333
def cmMinor12Matrix L340
theorem cmMinor12_submatrix_eq L346
theorem det_cmMinor12Matrix L352
theorem cmCofactor3_12_eq_poly L358
def cmMinor11Matrix L365
theorem cmMinor11_submatrix_eq L371
theorem det_cmMinor11Matrix L377
theorem cmCofactor3_11_eq_poly L383
def cmMinor22Matrix L390
theorem cmMinor22_submatrix_eq L396
theorem det_cmMinor22Matrix L402
theorem cmCofactor3_22_eq_poly L408
def cmMinor33Matrix L415
theorem cmMinor33_submatrix_eq L421
theorem det_cmMinor33Matrix L427
theorem cmCofactor3_33_eq_poly L433
def cmMinor44Matrix L440
theorem cmMinor44_submatrix_eq L446
theorem det_cmMinor44Matrix L452
theorem cmCofactor3_44_eq_poly L458
theorem cmCofactor3_opposite_eq_poly L466
theorem cmCofactor3_opposite_diag_eq_poly L479
def cmMinor00Matrix L498
theorem cmMinor00_submatrix_eq L504
theorem det_cmMinor00Matrix L510
theorem cmCofactor3_00_eq_poly L516
def cmMinor01Matrix L522
theorem cmMinor01_submatrix_eq L528
theorem det_cmMinor01Matrix L534
theorem cmCofactor3_01_eq_poly L540
def cmMinor02Matrix L546
theorem cmMinor02_submatrix_eq L552
theorem det_cmMinor02Matrix L558
theorem cmCofactor3_02_eq_poly L564
def cmMinor03Matrix L570
theorem cmMinor03_submatrix_eq L576
theorem det_cmMinor03Matrix L582
theorem cmCofactor3_03_eq_poly L588
def cmMinor04Matrix L594
theorem cmMinor04_submatrix_eq L600
theorem det_cmMinor04Matrix L606
theorem cmCofactor3_04_eq_poly L612
def cmMinor10Matrix L618
theorem cmMinor10_submatrix_eq L624
theorem det_cmMinor10Matrix L630
theorem cmCofactor3_10_eq_poly L636
def cmMinor20Matrix L642
theorem cmMinor20_submatrix_eq L648
theorem det_cmMinor20Matrix L654
theorem cmCofactor3_20_eq_poly L660
def cmMinor21Matrix L666
theorem cmMinor21_submatrix_eq L672
theorem det_cmMinor21Matrix L678
theorem cmCofactor3_21_eq_poly L684
def cmMinor30Matrix L690
theorem cmMinor30_submatrix_eq L696
theorem det_cmMinor30Matrix L702

… and 36 more