OAI/Combinatorics/StripMass/PfaffianMatrices.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. abbrev OAI.StripPfaffian.Vec line 14
  2. abbrev OAI.StripPfaffian.Grassmann line 15
  3. def OAI.StripPfaffian.standardBasis line 17
  4. def OAI.StripPfaffian.generator line 18
  5. def OAI.StripPfaffian.twoForm line 20
  6. def OAI.StripPfaffian.pfaffian line 22
  7. def OAI.StripPfaffian.d line 26
  8. def OAI.StripPfaffian.rho line 27
  9. def OAI.StripPfaffian.D line 28
  10. def OAI.StripPfaffian.kernel line 29
  11. def OAI.StripPfaffian.pfSize line 31
  12. def OAI.StripPfaffian.augmentedKernel line 32
  13. def OAI.StripPfaffian.p line 37
  14. def OAI.StripPfaffian.topWedge line 43
  15. def OAI.StripPfaffian.topCoord line 44
  16. lemma OAI.StripPfaffian.top_wedge_determinant line 47
  17. lemma OAI.StripPfaffian.generator_mem line 59
  18. lemma OAI.StripPfaffian.twoForm_mem line 63
  19. lemma OAI.StripPfaffian.twoForm_pow_mem line 73
  20. lemma OAI.StripPfaffian.exteriorBasis_univ line 78
  21. lemma OAI.StripPfaffian.topCoord_topWedge line 91
  22. lemma OAI.StripPfaffian.topCoord_wedge line 95
  23. lemma OAI.StripPfaffian.homogeneous_eq_coord_topWedge line 99
  24. lemma OAI.StripPfaffian.topCoord_map line 113
  25. lemma OAI.StripPfaffian.generator_anticomm line 124
  26. lemma OAI.StripPfaffian.sum_symmetric_offdiag line 128
  27. lemma OAI.StripPfaffian.twoForm_full line 156
  28. def OAI.StripPfaffian.permMap line 168
  29. lemma OAI.StripPfaffian.permMap_basis line 171
  30. lemma OAI.StripPfaffian.permMap_generator line 175
  31. lemma OAI.StripPfaffian.permMap_det line 179
  32. lemma OAI.StripPfaffian.twoForm_perm line 188
  33. lemma OAI.StripPfaffian.pfaffian_perm line 202
  34. lemma OAI.StripPfaffian.pfaffian_duplicate line 214
  35. lemma OAI.StripPfaffian.wedge_anticomm line 239
  36. lemma OAI.StripPfaffian.wedge_commutes line 244
  37. lemma OAI.StripPfaffian.twoForm_commutes line 263
  38. lemma OAI.StripPfaffian.wedge_sq_zero line 272
  39. lemma OAI.StripPfaffian.twoForm_add line 278
  40. lemma OAI.StripPfaffian.twoForm_smul line 282
  41. lemma OAI.StripPfaffian.generator_expansion line 286
  42. def OAI.StripPfaffian.rankTwo line 291
  43. lemma OAI.StripPfaffian.rankTwo_skew line 294
  44. lemma OAI.StripPfaffian.twoForm_rankTwo line 299
  45. lemma OAI.StripPfaffian.pow_add_sq_zero line 308
  46. lemma OAI.StripPfaffian.high_degree_zero line 323
  47. def OAI.StripPfaffian.embedMap line 338
  48. lemma OAI.StripPfaffian.embedMap_basis line 341
  49. lemma OAI.StripPfaffian.embedMap_generator line 345
  50. lemma OAI.StripPfaffian.embedMap_apply line 349
  51. def OAI.StripPfaffian.border line 357
  52. lemma OAI.StripPfaffian.border_old_old line 362
  53. lemma OAI.StripPfaffian.border_old_last line 364
  54. lemma OAI.StripPfaffian.border_last_old line 366
  55. lemma OAI.StripPfaffian.border_last_last line 368
  56. lemma OAI.StripPfaffian.border_skew line 371
  57. lemma OAI.StripPfaffian.twoForm_border line 380
  58. lemma OAI.StripPfaffian.topWedge_snoc line 406
  59. lemma OAI.StripPfaffian.topCoord_embed_mul_last line 415
  60. def OAI.StripPfaffian.borderLinear line 423