OAI/Computability/PerfectCompleteness/Algebra/FunctionSpaceLowerRank.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.FunctionSpaceLowerRank.transportForm line 24
  2. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.transportForm_apply line 28
  3. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.transportForm_rank line 32
  4. def OAI.PerfectCompleteness.FunctionSpaceLowerRank.matrixForm line 47
  5. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.matrixForm_rank line 52
  6. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.testedGram_matrixForm line 57
  7. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.testedGram_multiplicationForm line 62
  8. def OAI.PerfectCompleteness.FunctionSpaceLowerRank.displayedRows line 81
  9. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.displayedRows_products line 85
  10. def OAI.PerfectCompleteness.FunctionSpaceLowerRank.testedProductSpan line 92
  11. def OAI.PerfectCompleteness.FunctionSpaceLowerRank.IsLegalExtension line 97
  12. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.legal_extension_tested_rank_le_one line 104
  13. theorem OAI.PerfectCompleteness.FunctionSpaceLowerRank.high_rank_agreement_lt_of_legal_extensions line 121