OAI/Algebra/Determinantal/RowIdeals.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.AdjugateAlgebra.rowMultiplier line 10
  2. def OAI.PermanentBorder.AdjugateAlgebra.rowPair line 12
  3. def OAI.PermanentBorder.AdjugateAlgebra.rowEntry line 15
  4. def OAI.PermanentBorder.AdjugateAlgebra.rowIdeal line 18
  5. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_eq_sum line 21
  6. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_add line 26
  7. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_smul line 30
  8. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_zero line 34
  9. theorem OAI.PermanentBorder.AdjugateAlgebra.adjTrace_mul_comm line 36
  10. theorem OAI.PermanentBorder.AdjugateAlgebra.X_mul_rowPair line 42
  11. def OAI.PermanentBorder.AdjugateAlgebra.HasRowNormalForm line 54
  12. theorem OAI.PermanentBorder.AdjugateAlgebra.HasRowNormalForm.zero line 59
  13. theorem OAI.PermanentBorder.AdjugateAlgebra.HasRowNormalForm.add line 60
  14. theorem OAI.PermanentBorder.AdjugateAlgebra.HasRowNormalForm.C_mul line 65
  15. theorem OAI.PermanentBorder.AdjugateAlgebra.HasRowNormalForm.X_mul line 69
  16. theorem OAI.PermanentBorder.AdjugateAlgebra.HasRowNormalForm.mul line 74
  17. theorem OAI.PermanentBorder.AdjugateAlgebra.normalForm_of_mem_rowIdeal line 85
  18. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_degree_le line 104
  19. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_row_multiplier line 108
  20. theorem OAI.PermanentBorder.AdjugateAlgebra.row_multiplier_is_constant line 127
  21. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_constant_row_multiplier line 150
  22. def OAI.PermanentBorder.AdjugateAlgebra.rowContraction line 166
  23. theorem OAI.PermanentBorder.AdjugateAlgebra.rowContraction_mem line 170
  24. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_rowEntry line 178
  25. theorem OAI.PermanentBorder.AdjugateAlgebra.totalDegreeLE_rowContraction line 183
  26. theorem OAI.PermanentBorder.AdjugateAlgebra.rowContraction_top line 192
  27. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_rowContraction_top line 202
  28. theorem OAI.PermanentBorder.AdjugateAlgebra.exists_lower_row_representative line 215
  29. theorem OAI.PermanentBorder.AdjugateAlgebra.rowIdeal_low_degree_zero line 231
  30. theorem OAI.PermanentBorder.AdjugateAlgebra.row_quotient_spanned line 252
  31. theorem OAI.PermanentBorder.AdjugateAlgebra.finite_row_quotient line 313
  32. theorem OAI.PermanentBorder.AdjugateAlgebra.row_quotient_finrank line 325
  33. theorem OAI.PermanentBorder.AdjugateAlgebra.rowContraction_single line 357
  34. theorem OAI.PermanentBorder.AdjugateAlgebra.rowEntry_top line 363
  35. theorem OAI.PermanentBorder.AdjugateAlgebra.rowEntry_eq_of_rowIdeal_eq line 369
  36. theorem OAI.PermanentBorder.AdjugateAlgebra.rowContraction_eq_zero_iff line 384
  37. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_sub line 400
  38. theorem OAI.PermanentBorder.AdjugateAlgebra.rowPair_neg line 405
  39. theorem OAI.PermanentBorder.AdjugateAlgebra.matrix_eq_of_rowIdeal_eq line 409