OAI/Combinatorics/ThinTrees/Pencil/MatrixConstraintRealization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Matrix constraint realization.

  1. def OAI.CurrentKS.Realization.Realizes.sumIndexedMatrices line 16
  2. instance OAI.CurrentKS.Realization.poly_sumIndexedMatrices line 25
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.rat_matrixForm line 38
  4. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.triangleAt line 51
  5. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.triangleMatrixProgram line 56
  6. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_triangleMatrixProgram line 70
  7. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.weightedTriangle line 94
  8. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.weightedTriangleProgram line 97
  9. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_weightedTriangleProgram line 105
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.weightedTriangle_sum line 108
  11. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.triangleSum line 124
  12. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_triangleSum line 129
  13. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.lowerMatrix line 131
  14. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_lowerMatrix line 138
  15. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.upperMatrix line 140
  16. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_upperMatrix line 154
  17. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.edgeMatrix line 156
  18. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_edgeMatrix line 176
  19. abbrev OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.matrixBlockEquiv line 206
  20. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.specialMatrix line 208
  21. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_specialMatrix line 221
  22. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.matrixConstraints line 223
  23. instance OAI.AlgorithmicThinTrees.MetricTests.RationalStep.Stack.poly_matrixConstraints line 227