OAI/NumberTheory/Catalan/Determinants/OddPhysicalMinorCounts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.InternalCatalan.oddPhysicalIndex line 15
  2. def OAI.InternalCatalan.oddPhysicalChoice line 17
  3. instance OAI.InternalCatalan.oddPhysicalChoice_fintype line 22
  4. def OAI.InternalCatalan.oddPhysicalExceptionalTag line 26
  5. def OAI.InternalCatalan.oddPhysicalVector line 33
  6. def OAI.InternalCatalan.oddPhysicalScalar line 42
  7. def OAI.InternalCatalan.oddPhysicalColumn line 49
  8. theorem OAI.InternalCatalan.oddPhysicalColumn_expansion line 58
  9. def OAI.InternalCatalan.oddPhysicalVectorMinor line 82
  10. theorem OAI.InternalCatalan.oddPhysicalMinor_expansion line 89
  11. theorem OAI.InternalCatalan.oddPhysicalVector_of_exceptional line 119
  12. theorem OAI.InternalCatalan.oddPhysicalVectorMinor_eq_zero_of_repeat line 132
  13. def OAI.InternalCatalan.oddPhysicalIsRetained line 160
  14. def OAI.InternalCatalan.oddPhysicalIsPaired line 164
  15. def OAI.InternalCatalan.oddPhysicalRetainedSet line 168
  16. def OAI.InternalCatalan.oddPhysicalPairedSet line 171
  17. def OAI.InternalCatalan.oddPhysicalExceptionalSet line 174
  18. def OAI.InternalCatalan.oddPhysicalLoss line 178
  19. theorem OAI.InternalCatalan.oddPhysical_one_tag line 184
  20. theorem OAI.InternalCatalan.oddPhysical_counts_le_size line 194
  21. theorem OAI.InternalCatalan.oddPhysical_retained_count_le line 204
  22. theorem OAI.InternalCatalan.oddPhysical_paired_count_le line 220
  23. theorem OAI.InternalCatalan.oddPhysical_exceptional_count_le line 238
  24. theorem OAI.InternalCatalan.oddPhysical_total_loss_eq line 266
  25. theorem OAI.InternalCatalan.oddPhysical_total_loss_le_min line 277