OAI/Algebra/FormulaHitting/Representation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NCHitting.automatonValue line 12
  2. theorem OAI.NCHitting.automatonValue_add line 17
  3. theorem OAI.NCHitting.automatonValue_smul line 25
  4. theorem OAI.NCHitting.automatonValue_zero line 32
  5. def OAI.NCHitting.wordMatrix line 39
  6. theorem OAI.NCHitting.automatonValue_eq_matrix line 43
  7. theorem OAI.NCHitting.automatonValue_sumBlocks line 53
  8. def OAI.NCHitting.productTransition line 66
  9. theorem OAI.NCHitting.automatonValue_productBlocks_general line 72
  10. theorem OAI.NCHitting.automatonValue_productBlocks line 92
  11. structure OAI.NCHitting.AcyclicRepresentation line 101
  12. def OAI.NCHitting.AcyclicRepresentation.value line 118
  13. theorem OAI.NCHitting.AcyclicRepresentation.wordMatrix_entry_zero line 121
  14. theorem OAI.NCHitting.AcyclicRepresentation.wordMatrix_eq_zero line 139
  15. theorem OAI.NCHitting.AcyclicRepresentation.value_eq_matrix line 146
  16. def OAI.NCHitting.AcyclicRepresentation.sumRank line 150
  17. theorem OAI.NCHitting.AcyclicRepresentation.sumRank_lt line 153
  18. theorem OAI.NCHitting.AcyclicRepresentation.block_upper line 165
  19. def OAI.NCHitting.AcyclicRepresentation.add line 185
  20. theorem OAI.NCHitting.AcyclicRepresentation.add_value line 196
  21. def OAI.NCHitting.AcyclicRepresentation.mul line 200
  22. theorem OAI.NCHitting.AcyclicRepresentation.mul_value line 211
  23. def OAI.NCHitting.AcyclicRepresentation.scalar line 215
  24. theorem OAI.NCHitting.AcyclicRepresentation.scalar_value line 226
  25. def OAI.NCHitting.AcyclicRepresentation.ofVariable line 237
  26. theorem OAI.NCHitting.AcyclicRepresentation.variable_value line 252
  27. theorem OAI.NCHitting.AcyclicRepresentation.scalar_card line 280
  28. theorem OAI.NCHitting.AcyclicRepresentation.variable_card line 282
  29. theorem OAI.NCHitting.AcyclicRepresentation.add_card line 285
  30. theorem OAI.NCHitting.AcyclicRepresentation.mul_card line 289
  31. def OAI.NCHitting.Formula.representation line 295
  32. theorem OAI.NCHitting.Formula.representation_card_le line 302
  33. theorem OAI.NCHitting.Formula.representation_card_pos line 318
  34. theorem OAI.NCHitting.Formula.representation_correct line 332
  35. theorem OAI.NCHitting.Formula.coeff_zero_of_representation_dimension_le line 344