OAI/NumberTheory/Catalan/Determinants/OddLowerMinorTransfer.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.InternalCatalan.oddLowerRetainedSize line 14
  2. abbrev OAI.InternalCatalan.oddLowerPairedSize line 15
  3. abbrev OAI.InternalCatalan.oddLowerPhysicalIndex line 16
  4. def OAI.InternalCatalan.oddLowerRetainedTag line 19
  5. def OAI.InternalCatalan.oddLowerPairedTag line 22
  6. def OAI.InternalCatalan.oddLowerRetainedVector line 25
  7. def OAI.InternalCatalan.oddLowerPairedVector line 30
  8. def OAI.InternalCatalan.oddLowerPhysicalColumn line 35
  9. theorem OAI.InternalCatalan.oddLowerPhysicalColumn_retained line 41
  10. theorem OAI.InternalCatalan.oddLowerPhysicalColumn_paired line 49
  11. theorem OAI.InternalCatalan.oddLowerRetainedVector_den_ne_zero line 58
  12. theorem OAI.InternalCatalan.oddLowerPairedVector_den_ne_zero line 68
  13. theorem OAI.InternalCatalan.oddLowerHighSet_sub_mem_pair line 79
  14. def OAI.InternalCatalan.oddLowerInverseCoeff line 84
  15. theorem OAI.InternalCatalan.rawEntryRat_eq_lower_physical_sum line 96
  16. theorem OAI.InternalCatalan.oddLowerPhysical_loss_eq line 126
  17. theorem OAI.InternalCatalan.oddLowerPhysicalCombination_valuation_lower line 136
  18. theorem OAI.InternalCatalan.rawMinorRat_odd_lower_valuation line 156
  19. theorem OAI.InternalCatalan.determinantRat_odd_lower_valuation line 171
  20. theorem OAI.InternalCatalan.determinantRat_odd_lower_loss line 184