OAI/Algebra/Determinantal/AdjugateNormalForm.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.AdjugateAlgebra.trace_commutator_adjugate line 11
  2. theorem OAI.PermanentBorder.AdjugateAlgebra.trace_commutator_adjugate_scalar line 17
  3. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_diagonal_commutator line 31
  4. theorem OAI.PermanentBorder.AdjugateAlgebra.natDegree_adjugate_linear_le line 50
  5. theorem OAI.PermanentBorder.AdjugateAlgebra.coeff_adjugate_linear line 70
  6. def OAI.PermanentBorder.AdjugateAlgebra.spectralSlope line 89
  7. theorem OAI.PermanentBorder.AdjugateAlgebra.diagonal_zero_of_trace_slope line 92
  8. def OAI.PermanentBorder.AdjugateAlgebra.pencilBase line 125
  9. def OAI.PermanentBorder.AdjugateAlgebra.scaledPencil line 130
  10. def OAI.PermanentBorder.AdjugateAlgebra.liftCoefficients line 135
  11. def OAI.PermanentBorder.AdjugateAlgebra.scaledTrace line 137
  12. theorem OAI.PermanentBorder.AdjugateAlgebra.scaledPencil_eq line 142
  13. theorem OAI.PermanentBorder.AdjugateAlgebra.scaledTrace_commutator line 153
  14. theorem OAI.PermanentBorder.AdjugateAlgebra.coeff_scaledTrace_top line 168
  15. theorem OAI.PermanentBorder.AdjugateAlgebra.diagonal_top_zero line 188
  16. theorem OAI.PermanentBorder.AdjugateAlgebra.scaledTrace_sub line 199
  17. theorem OAI.PermanentBorder.AdjugateAlgebra.pencil_commutator_expand line 208
  18. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_lower_multiplier line 219
  19. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_constant_multiplier_of_bounded_scaledTrace line 252
  20. def OAI.PermanentBorder.AdjugateAlgebra.pencilMatrix line 279
  21. def OAI.PermanentBorder.AdjugateAlgebra.adjTrace line 282
  22. theorem OAI.PermanentBorder.AdjugateAlgebra.adjTrace_zero line 285
  23. theorem OAI.PermanentBorder.AdjugateAlgebra.adjTrace_add line 288
  24. theorem OAI.PermanentBorder.AdjugateAlgebra.adjTrace_neg line 293
  25. theorem OAI.PermanentBorder.AdjugateAlgebra.adjTrace_smul line 297
  26. theorem OAI.PermanentBorder.AdjugateAlgebra.X_mul_adjTrace line 305
  27. def OAI.PermanentBorder.AdjugateAlgebra.HasAdjugateNormalForm line 328
  28. theorem OAI.PermanentBorder.AdjugateAlgebra.HasAdjugateNormalForm.zero line 334
  29. theorem OAI.PermanentBorder.AdjugateAlgebra.HasAdjugateNormalForm.add line 337
  30. theorem OAI.PermanentBorder.AdjugateAlgebra.HasAdjugateNormalForm.C_mul line 345
  31. theorem OAI.PermanentBorder.AdjugateAlgebra.HasAdjugateNormalForm.X_mul line 352
  32. theorem OAI.PermanentBorder.AdjugateAlgebra.HasAdjugateNormalForm.mul line 359
  33. def OAI.PermanentBorder.AdjugateAlgebra.cofactorIdeal line 372
  34. theorem OAI.PermanentBorder.AdjugateAlgebra.normalForm_of_mem_cofactorIdeal line 375
  35. theorem OAI.PermanentBorder.AdjugateAlgebra.natDegree_adjTrace_le line 397
  36. theorem OAI.PermanentBorder.AdjugateAlgebra.natDegree_det_pencilMatrix line 412
  37. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_multiplier_of_mem_cofactorIdeal line 424
  38. def OAI.PermanentBorder.AdjugateAlgebra.scaleHom line 449
  39. theorem OAI.PermanentBorder.AdjugateAlgebra.scaleHom_C line 452
  40. theorem OAI.PermanentBorder.AdjugateAlgebra.scaleHom_X line 455
  41. theorem OAI.PermanentBorder.AdjugateAlgebra.scaleHom_injective line 459
  42. theorem OAI.PermanentBorder.AdjugateAlgebra.scaleHom_pencil line 472
  43. theorem OAI.PermanentBorder.AdjugateAlgebra.scaleHom_adjTrace line 482
  44. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_constant_multiplier_of_mem_cofactorIdeal line 496
  45. theorem OAI.PermanentBorder.AdjugateAlgebra.scaleHom_monomial_monomial line 514
  46. theorem OAI.PermanentBorder.AdjugateAlgebra.coeff_scaleHom line 521
  47. def OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE line 547
  48. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.outer line 550
  49. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.scaled line 557
  50. theorem OAI.PermanentBorder.AdjugateAlgebra.adjugate_generation line 567
  51. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_iff_scaled_natDegree line 574
  52. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.mul line 583
  53. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.mono line 589
  54. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_monomial line 593
  55. theorem OAI.PermanentBorder.AdjugateAlgebra.coeff_adjTrace_eq_zero line 598
  56. theorem OAI.PermanentBorder.AdjugateAlgebra.critical_ideal_eq_zero line 606
  57. abbrev OAI.PermanentBorder.AdjugateAlgebra.PlaneIndex line 635
  58. theorem OAI.PermanentBorder.AdjugateAlgebra.card_planeIndex line 637
  59. def OAI.PermanentBorder.AdjugateAlgebra.planeMap line 641
  60. theorem OAI.PermanentBorder.AdjugateAlgebra.coeff_planeMap line 646
  61. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_planeMap line 671
  62. theorem OAI.PermanentBorder.AdjugateAlgebra.critical_cofactor_length line 687
  63. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_cofactor line 711
  64. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.add line 723
  65. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.sub line 728
  66. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.sum line 733
  67. def OAI.PermanentBorder.AdjugateAlgebra.diagonalContraction line 739
  68. theorem OAI.PermanentBorder.AdjugateAlgebra.diagonalContraction_eq_sum line 743
  69. theorem OAI.PermanentBorder.AdjugateAlgebra.diagonalContraction_mem line 750
  70. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_diagonalContraction line 759
  71. def OAI.PermanentBorder.AdjugateAlgebra.slopeTrace line 768
  72. theorem OAI.PermanentBorder.AdjugateAlgebra.natDegree_adjugate_slope_le line 771
  73. theorem OAI.PermanentBorder.AdjugateAlgebra.natDegree_slopeTrace_le line 783
  74. def OAI.PermanentBorder.AdjugateAlgebra.slopeCoefficientMap line 793
  75. theorem OAI.PermanentBorder.AdjugateAlgebra.slopeCoefficientMap_injective line 805
  76. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_diagonalContraction_top line 820
  77. theorem OAI.PermanentBorder.AdjugateAlgebra.TotalDegreeLE.pred_of_top_zero line 839
  78. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_lower_monomial_representative line 851
  79. theorem OAI.PermanentBorder.AdjugateAlgebra.eq_sum_bivariate line 867
  80. theorem OAI.PermanentBorder.AdjugateAlgebra.map_mem_of_monomials line 878
  81. theorem OAI.PermanentBorder.AdjugateAlgebra.cofactor_quotient_spanned line 891
  82. theorem OAI.PermanentBorder.AdjugateAlgebra.finite_cofactor_quotient line 952