OAI/Analysis/Quantum/DimensionTen/MinorData.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.Border.pencilR line 11
  2. def OAI.DimensionTen.Border.rowChoices line 14
  3. def OAI.DimensionTen.Border.minor line 16
  4. def OAI.DimensionTen.Border.homogeneousLow line 19
  5. def OAI.DimensionTen.Border.pencilExplicit line 23
  6. lemma OAI.DimensionTen.Border.pencil_entry_0_0 line 26
  7. lemma OAI.DimensionTen.Border.pencil_entry_0_1 line 34
  8. lemma OAI.DimensionTen.Border.pencil_entry_0_2 line 42
  9. lemma OAI.DimensionTen.Border.pencil_entry_0_3 line 50
  10. lemma OAI.DimensionTen.Border.pencil_entry_1_0 line 58
  11. lemma OAI.DimensionTen.Border.pencil_entry_1_1 line 66
  12. lemma OAI.DimensionTen.Border.pencil_entry_1_2 line 74
  13. lemma OAI.DimensionTen.Border.pencil_entry_1_3 line 82
  14. lemma OAI.DimensionTen.Border.pencil_entry_2_0 line 90
  15. lemma OAI.DimensionTen.Border.pencil_entry_2_1 line 98
  16. lemma OAI.DimensionTen.Border.pencil_entry_2_2 line 106
  17. lemma OAI.DimensionTen.Border.pencil_entry_2_3 line 114
  18. lemma OAI.DimensionTen.Border.pencil_entry_3_0 line 122
  19. lemma OAI.DimensionTen.Border.pencil_entry_3_1 line 130
  20. lemma OAI.DimensionTen.Border.pencil_entry_3_2 line 138
  21. lemma OAI.DimensionTen.Border.pencil_entry_3_3 line 146
  22. lemma OAI.DimensionTen.Border.pencil_entry_4_0 line 154
  23. lemma OAI.DimensionTen.Border.pencil_entry_4_1 line 162
  24. lemma OAI.DimensionTen.Border.pencil_entry_4_2 line 170
  25. lemma OAI.DimensionTen.Border.pencil_entry_4_3 line 178
  26. lemma OAI.DimensionTen.Border.pencil_entry_5_0 line 186
  27. lemma OAI.DimensionTen.Border.pencil_entry_5_1 line 194
  28. lemma OAI.DimensionTen.Border.pencil_entry_5_2 line 202
  29. lemma OAI.DimensionTen.Border.pencil_entry_5_3 line 210
  30. lemma OAI.DimensionTen.Border.pencilR_eq line 218
  31. lemma OAI.DimensionTen.Border.det_four line 246
  32. lemma OAI.DimensionTen.Border.homogeneousLow_eq line 253
  33. lemma OAI.DimensionTen.Border.high_eq line 257
  34. lemma OAI.DimensionTen.Border.minors_row_0 line 261
  35. lemma OAI.DimensionTen.Border.minors_row_1 line 271
  36. lemma OAI.DimensionTen.Border.minors_row_2 line 281
  37. lemma OAI.DimensionTen.Border.minors_row_3 line 291
  38. lemma OAI.DimensionTen.Border.minors_row_4 line 301
  39. lemma OAI.DimensionTen.Border.minors_row_5 line 311
  40. lemma OAI.DimensionTen.Border.minors_row_6 line 321
  41. lemma OAI.DimensionTen.Border.minors_row_7 line 331
  42. lemma OAI.DimensionTen.Border.minors_row_8 line 341
  43. lemma OAI.DimensionTen.Border.minors_row_9 line 351
  44. lemma OAI.DimensionTen.Border.minors_row_10 line 361
  45. lemma OAI.DimensionTen.Border.minors_row_11 line 371
  46. lemma OAI.DimensionTen.Border.minors_row_12 line 381
  47. lemma OAI.DimensionTen.Border.minors_row_13 line 391
  48. lemma OAI.DimensionTen.Border.minors_row_14 line 401