OAI/Algebra/FormulaHitting/System.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NCHitting.AcyclicRepresentation.J_sum line 17
  2. theorem OAI.NCHitting.AcyclicRepresentation.J_C_mul line 25
  3. def OAI.NCHitting.AcyclicRepresentation.systemLevel line 29
  4. def OAI.NCHitting.AcyclicRepresentation.systemMatrix line 35
  5. def OAI.NCHitting.AcyclicRepresentation.fundamentalMatrix line 39
  6. def OAI.NCHitting.AcyclicRepresentation.denominator line 43
  7. def OAI.NCHitting.AcyclicRepresentation.cofactor line 46
  8. def OAI.NCHitting.AcyclicRepresentation.systemNumerator line 49
  9. theorem OAI.NCHitting.AcyclicRepresentation.denominator_eq line 54
  10. theorem OAI.NCHitting.AcyclicRepresentation.denominator_degree line 59
  11. theorem OAI.NCHitting.AcyclicRepresentation.cofactor_degree line 65
  12. theorem OAI.NCHitting.AcyclicRepresentation.systemNumerator_degree line 71
  13. theorem OAI.NCHitting.AcyclicRepresentation.denominator_eval_zero_ne line 77
  14. theorem OAI.NCHitting.AcyclicRepresentation.denominator_mul_kernel line 84
  15. theorem OAI.NCHitting.AcyclicRepresentation.polynomial_coe_sum line 97
  16. theorem OAI.NCHitting.AcyclicRepresentation.denominator_mul_systemMatrix line 101
  17. theorem OAI.NCHitting.AcyclicRepresentation.systemLevel_wordSum line 111
  18. def OAI.NCHitting.AcyclicRepresentation.contract line 128
  19. theorem OAI.NCHitting.AcyclicRepresentation.contract_eq_sum line 136
  20. theorem OAI.NCHitting.AcyclicRepresentation.contract_wordMatrix line 150
  21. theorem OAI.NCHitting.AcyclicRepresentation.systemLevel_eq_sum line 156
  22. theorem OAI.NCHitting.AcyclicRepresentation.fundamentalMatrix_eq_sum line 165
  23. theorem OAI.NCHitting.AcyclicRepresentation.contract_fundamentalMatrix line 173
  24. theorem OAI.NCHitting.AcyclicRepresentation.systemLevel_constant_zero line 181
  25. theorem OAI.NCHitting.AcyclicRepresentation.systemLevel_entry_zero line 187
  26. theorem OAI.NCHitting.AcyclicRepresentation.systemLevel_eq_zero line 207
  27. theorem OAI.NCHitting.AcyclicRepresentation.derivative_systemLevel line 215
  28. theorem OAI.NCHitting.AcyclicRepresentation.fundamentalMatrix_constant line 230
  29. theorem OAI.NCHitting.AcyclicRepresentation.fundamentalMatrix_isUnit line 241
  30. theorem OAI.NCHitting.AcyclicRepresentation.fundamentalMatrix_derivative line 252
  31. theorem OAI.NCHitting.AcyclicRepresentation.fundamentalMatrix_polynomial_system line 274
  32. theorem OAI.NCHitting.Formula.system_output line 290