OAI/Combinatorics/StripMass/InterpolantCovariance.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.topPerm_symm line 14
  2. lemma OAI.CriticalStrip.Diagram.permLaurent_lift line 20
  3. lemma OAI.CriticalStrip.Diagram.permSpectral_lift line 30
  4. lemma OAI.CriticalStrip.Diagram.localR_map_hom line 40
  5. lemma OAI.CriticalStrip.Diagram.permSpectral_interpolant line 50
  6. theorem OAI.CriticalStrip.Diagram.rationalInterpolant_covariance line 62
  7. theorem OAI.CriticalStrip.Diagram.pfaffian_eq_zero_of_equal_rows line 107
  8. def OAI.CriticalStrip.Diagram.replaceFirst line 129
  9. theorem OAI.CriticalStrip.Diagram.replaceFirst_row line 134
  10. theorem OAI.CriticalStrip.Diagram.replaceFirst_rest line 138
  11. theorem OAI.CriticalStrip.Diagram.replaceFirst_skew line 143
  12. theorem OAI.CriticalStrip.Diagram.pfaffian_replaceFirst_add line 151
  13. theorem OAI.CriticalStrip.Diagram.pfaffian_replaceFirst_smul line 164
  14. theorem OAI.CriticalStrip.Diagram.skew_diagonal_zero line 176
  15. theorem OAI.CriticalStrip.Diagram.pfaffian_replaceFirst_otherRow line 185
  16. theorem OAI.CriticalStrip.Diagram.pfaffian_firstRow_add_other line 198
  17. def OAI.CriticalStrip.Diagram.frontBorder line 234
  18. def OAI.CriticalStrip.Diagram.backBorder line 239
  19. theorem OAI.CriticalStrip.Diagram.frontBorder_zero_zero line 244
  20. theorem OAI.CriticalStrip.Diagram.frontBorder_zero_succ line 246
  21. theorem OAI.CriticalStrip.Diagram.frontBorder_succ_zero line 248
  22. theorem OAI.CriticalStrip.Diagram.frontBorder_succ_succ line 250
  23. theorem OAI.CriticalStrip.Diagram.backBorder_last_last line 253
  24. theorem OAI.CriticalStrip.Diagram.backBorder_cast_last line 256
  25. theorem OAI.CriticalStrip.Diagram.backBorder_last_cast line 259
  26. theorem OAI.CriticalStrip.Diagram.backBorder_cast_cast line 262
  27. theorem OAI.CriticalStrip.Diagram.frontBorder_skew line 266
  28. theorem OAI.CriticalStrip.Diagram.backBorder_skew line 275
  29. theorem OAI.CriticalStrip.Diagram.rotateInv_zero line 284
  30. theorem OAI.CriticalStrip.Diagram.rotateInv_succ line 288
  31. theorem OAI.CriticalStrip.Diagram.backBorder_rotate line 294
  32. theorem OAI.CriticalStrip.Diagram.pfaffian_frontBorder_scale line 304
  33. theorem OAI.CriticalStrip.Diagram.pfaffian_front_back line 324
  34. def OAI.CriticalStrip.Diagram.tailRotateInv line 342
  35. theorem OAI.CriticalStrip.Diagram.tailRotateInv_zero line 345
  36. theorem OAI.CriticalStrip.Diagram.tailRotateInv_one line 347
  37. theorem OAI.CriticalStrip.Diagram.tailRotateInv_succ_succ line 350
  38. theorem OAI.CriticalStrip.Diagram.sign_tailRotateInv line 355
  39. theorem OAI.CriticalStrip.Diagram.pfaffian_doubleBorder line 362
  40. theorem OAI.CriticalStrip.Diagram.back_front_row line 419
  41. theorem OAI.CriticalStrip.Diagram.back_front_tail line 427
  42. theorem OAI.CriticalStrip.Diagram.back_front_eq_rowAdd line 434
  43. theorem OAI.CriticalStrip.Diagram.pfaffian_back_front line 467
  44. def OAI.CriticalStrip.Diagram.plainKernel line 475
  45. theorem OAI.CriticalStrip.Diagram.plainKernel_skew line 479
  46. theorem OAI.CriticalStrip.Diagram.pfaffian_augmented_even line 488
  47. theorem OAI.CriticalStrip.Diagram.pfaffian_augmented_odd line 497