OAI/Combinatorics/ContingencyTables/Machines/MatrixSubtractProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Entrywise natural subtraction on a supplied matrix shape

  1. abbrev OAI.ContingencyTables.MatrixSubtractProgram.Input line 13
  2. abbrev OAI.ContingencyTables.MatrixSubtractProgram.RowInput line 14
  3. def OAI.ContingencyTables.MatrixSubtractProgram.entry line 16
  4. def OAI.ContingencyTables.MatrixSubtractProgram.entryRealizer line 18
  5. lemma OAI.ContingencyTables.MatrixSubtractProgram.polynomial_entry line 30
  6. def OAI.ContingencyTables.MatrixSubtractProgram.sourceRow line 44
  7. def OAI.ContingencyTables.MatrixSubtractProgram.sourceRowRealizer line 45
  8. lemma OAI.ContingencyTables.MatrixSubtractProgram.polynomial_sourceRow line 47
  9. def OAI.ContingencyTables.MatrixSubtractProgram.columns line 52
  10. def OAI.ContingencyTables.MatrixSubtractProgram.columnsRealizer line 53
  11. lemma OAI.ContingencyTables.MatrixSubtractProgram.polynomial_columns line 56
  12. def OAI.ContingencyTables.MatrixSubtractProgram.row line 62
  13. def OAI.ContingencyTables.MatrixSubtractProgram.rowRealizer line 63
  14. lemma OAI.ContingencyTables.MatrixSubtractProgram.polynomial_row line 65
  15. def OAI.ContingencyTables.MatrixSubtractProgram.indices line 69
  16. def OAI.ContingencyTables.MatrixSubtractProgram.indicesRealizer line 70
  17. lemma OAI.ContingencyTables.MatrixSubtractProgram.polynomial_indices line 71
  18. def OAI.ContingencyTables.MatrixSubtractProgram.matrix line 77
  19. def OAI.ContingencyTables.MatrixSubtractProgram.matrixRealizer line 78
  20. theorem OAI.ContingencyTables.MatrixSubtractProgram.polynomial_matrix line 80
  21. theorem OAI.ContingencyTables.MatrixSubtractProgram.matrix_code line 84