OAI/Computability/PerfectCompleteness/Algebra/MatrixRowQuotientLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.MatrixRowQuotientLaw.projectMatrixLinear line 22
  2. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.projectMatrixLinear_apply line 34
  3. def OAI.PerfectCompleteness.MatrixRowQuotientLaw.jointProjection line 38
  4. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.jointProjection_apply line 43
  5. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.jointProjection_surjective line 47
  6. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.uniform_product line 54
  7. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.uniform_jointProjection line 69
  8. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.independent_uniform_jointProjection line 76
  9. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.expect_prod line 84
  10. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.expect_project_matrix_increment line 90
  11. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.rankOne_pair_law line 107
  12. theorem OAI.PerfectCompleteness.MatrixRowQuotientLaw.expect_project_rankOne_pair line 123