OAI/Algebra/FormulaHitting/Generator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NCHitting.dimension_pos line 12
  2. theorem OAI.NCHitting.dimension_le line 17
  3. theorem OAI.NCHitting.dimension_eq line 25
  4. theorem OAI.NCHitting.dimension_one line 33
  5. theorem OAI.NCHitting.generator_one line 35
  6. theorem OAI.NCHitting.generator_entry line 38
  7. theorem OAI.NCHitting.matrixEntry_of_lt line 44
  8. theorem OAI.NCHitting.matrixEntry_of_le line 48
  9. def OAI.NCHitting.entryBitBound line 51
  10. theorem OAI.NCHitting.size_mul_le line 53
  11. theorem OAI.NCHitting.size_pow_le line 58
  12. theorem OAI.NCHitting.denominator_pos line 67
  13. theorem OAI.NCHitting.denominator_size_le line 70
  14. theorem OAI.NCHitting.size_le_self line 84
  15. theorem OAI.NCHitting.entryBitBound_le line 88