OAI/Combinatorics/StripMass/PfaffianEvaluation.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.StripPfaffian.clearedPf_eval line 13
  2. lemma OAI.StripPfaffian.clearedPf_root line 25
  3. def OAI.StripPfaffian.nodalPoly line 58
  4. lemma OAI.StripPfaffian.nodalPoly_monic line 60
  5. lemma OAI.StripPfaffian.nodalPoly_degree line 63
  6. lemma OAI.StripPfaffian.nodalPoly_dvd line 67
  7. lemma OAI.StripPfaffian.normalized_cleared_monic line 75
  8. def OAI.StripPfaffian.prefactor line 87
  9. lemma OAI.StripPfaffian.p_eq line 90
  10. lemma OAI.StripPfaffian.prod_Ioi_castSucc line 92
  11. lemma OAI.StripPfaffian.prod_Ioi_last line 99
  12. lemma OAI.StripPfaffian.prefactor_snoc line 108
  13. lemma OAI.StripPfaffian.nodalPoly_eval line 115
  14. lemma OAI.StripPfaffian.difference_prod line 119
  15. lemma OAI.StripPfaffian.generic_arch_quotient_factor line 128
  16. theorem OAI.StripPfaffian.generic_arch_quotient_monic line 168
  17. def OAI.StripPfaffian.flatC line 184
  18. def OAI.StripPfaffian.harmonicPoly line 185
  19. def OAI.StripPfaffian.Epoly line 186
  20. def OAI.StripPfaffian.perturbedRootC line 187
  21. def OAI.StripPfaffian.HasProjectionC line 189
  22. lemma OAI.StripPfaffian.constant_relations line 195
  23. def OAI.StripPfaffian.invariantFactor line 217
  24. def OAI.StripPfaffian.kernelProjectP line 219
  25. def OAI.StripPfaffian.kernelProjectJ line 222
  26. def OAI.StripPfaffian.kernelProjectE line 226
  27. lemma OAI.StripPfaffian.paired_invariant line 230
  28. lemma OAI.StripPfaffian.kernel_projection_identity line 238
  29. lemma OAI.StripPfaffian.HasProjectionC.zero line 257
  30. lemma OAI.StripPfaffian.HasProjectionC.add line 260
  31. lemma OAI.StripPfaffian.HasProjectionC.const_mul line 270
  32. lemma OAI.StripPfaffian.HasProjectionC.mul_comp line 282
  33. lemma OAI.StripPfaffian.HasProjectionC.sum line 298
  34. lemma OAI.StripPfaffian.base_projected line 308
  35. lemma OAI.StripPfaffian.kernel_projected line 311
  36. lemma OAI.StripPfaffian.invariant_product_degree line 317
  37. lemma OAI.StripPfaffian.paired_product line 327
  38. lemma OAI.StripPfaffian.denominator_projected line 334
  39. lemma OAI.StripPfaffian.numerator_projected line 340
  40. lemma OAI.StripPfaffian.polyLift_projected line 354
  41. lemma OAI.StripPfaffian.cleared_projected line 367
  42. theorem OAI.StripPfaffian.generic_pfaffian_projection line 376
  43. def OAI.StripComplexification.component line 403
  44. lemma OAI.StripComplexification.component_coeff line 406
  45. lemma OAI.StripComplexification.component_add line 409
  46. lemma OAI.StripComplexification.component_C line 414
  47. lemma OAI.StripComplexification.component_real_mul line 421