OAI/Combinatorics/ThinTrees/RationalMatrix/SchurHistory.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Schur history.

  1. def OAI.CurrentKS.Realization.SchurDesc line 19
  2. lemma OAI.CurrentKS.Realization.SchurDesc.refl line 23
  3. lemma OAI.CurrentKS.Realization.SchurDesc.dim line 26
  4. lemma OAI.CurrentKS.Realization.SchurDesc.psd line 31
  5. lemma OAI.CurrentKS.Realization.SchurDesc.schur line 37
  6. lemma OAI.CurrentKS.Realization.SchurDesc.wire line 51
  7. abbrev OAI.CurrentKS.Realization.SchurStack line 58
  8. abbrev OAI.CurrentKS.Realization.schurStackCode line 59
  9. def OAI.CurrentKS.Realization.schurNextData line 61
  10. abbrev OAI.CurrentKS.Realization.schurCurrent line 64
  11. abbrev OAI.CurrentKS.Realization.schurOld line 65
  12. def OAI.CurrentKS.Realization.schurNext line 67
  13. instance OAI.CurrentKS.Realization.poly_schurNext line 72
  14. def OAI.CurrentKS.Realization.schurHistoryData line 74
  15. lemma OAI.CurrentKS.Realization.schurHistory_length line 79
  16. lemma OAI.CurrentKS.Realization.schurHistory_iterate line 85
  17. def OAI.CurrentKS.Realization.schurHistory line 96
  18. lemma OAI.CurrentKS.Realization.schurNext_invariant line 101
  19. lemma OAI.CurrentKS.Realization.schurHistory_mem line 119
  20. lemma OAI.CurrentKS.Realization.runsPoly_schurHistory line 125