OAI/Combinatorics/ThinTrees/DeterminantCalculus.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.MSS.basePencil line 14
  2. def OAI.StrongThinTree.MSS.zeroSub line 17
  3. def OAI.StrongThinTree.MSS.zeroDiff line 20
  4. def OAI.StrongThinTree.MSS.view line 23
  5. lemma OAI.StrongThinTree.MSS.view_C line 28
  6. lemma OAI.StrongThinTree.MSS.view_X line 32
  7. lemma OAI.StrongThinTree.MSS.zeroSub_C line 37
  8. lemma OAI.StrongThinTree.MSS.zeroSub_X line 41
  9. lemma OAI.StrongThinTree.MSS.view_derivative line 46
  10. lemma OAI.StrongThinTree.MSS.view_zero line 58
  11. lemma OAI.StrongThinTree.MSS.zeroDiff_coeff line 69
  12. lemma OAI.StrongThinTree.MSS.view_affine_entry line 75
  13. lemma OAI.StrongThinTree.MSS.view_baseMatrix line 93
  14. lemma OAI.StrongThinTree.MSS.view_basePencil line 104
  15. lemma OAI.StrongThinTree.MSS.zeroDiff_basePencil line 113