OAI/Combinatorics/ThinTrees/RationalMatrix/MatrixRealization.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Matrix realization.

  1. lemma OAI.CurrentKS.Realization.runsPoly_fold_of_poly line 18
  2. abbrev OAI.CurrentKS.Realization.matrixView line 55
  3. instance OAI.CurrentKS.Realization.poly_matrixView line 59
  4. abbrev OAI.CurrentKS.Realization.matrixDim line 63
  5. abbrev OAI.CurrentKS.Realization.matrixEntries line 64
  6. lemma OAI.CurrentKS.Realization.matrix_entry_data line 66
  7. lemma OAI.CurrentKS.Realization.matrixCode_parts_bound line 71
  8. lemma OAI.CurrentKS.Realization.matrixObject_dim_le line 84
  9. lemma OAI.CurrentKS.Realization.matrixObject_parts line 88
  10. lemma OAI.CurrentKS.Realization.matrixObject_parts_bound line 96
  11. def OAI.CurrentKS.Realization.schurData line 106
  12. abbrev OAI.CurrentKS.Realization.entryCode line 111
  13. abbrev OAI.CurrentKS.Realization.entryBase line 112
  14. abbrev OAI.CurrentKS.Realization.entryI line 114
  15. abbrev OAI.CurrentKS.Realization.entryJ line 116
  16. def OAI.CurrentKS.Realization.schurEntry line 118
  17. instance OAI.CurrentKS.Realization.poly_schurEntry line 132
  18. def OAI.CurrentKS.Realization.schur line 134
  19. instance OAI.CurrentKS.Realization.poly_schur line 165