OAI/LinearAlgebra/MatrixFields/Histories/GroupOrbitTransport.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Counts line 26
  2. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Targets line 28
  3. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Pos line 30
  4. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Raw line 32
  5. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Orbit line 34
  6. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Variable line 36
  7. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.tripleSide line 39
  8. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.reorder line 42
  9. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.tripleSide_reorder line 45
  10. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.reorder_injective line 50
  11. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.reorder_support line 54
  12. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.coarse line 58
  13. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.ambient line 62
  14. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.support line 67
  15. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.counts_support line 71
  16. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.coarse_injective line 77
  17. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.ambient_support line 81
  18. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.coarse_mem_ambient line 87
  19. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.sharing line 97
  20. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.workComplement line 103
  21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.complement line 109
  22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.compatibilityLaw line 112
  23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.designated line 121
  24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.fineCompatible line 130
  25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.ownWord line 139
  26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Compatible line 143
  27. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.Admissible line 149
  28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.orbitOf line 157
  29. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.usedOrbits line 162
  30. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.full line 167
  31. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.passing line 172
  32. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.competitors line 177
  33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.full_pos line 186
  34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.competitor_mem line 193
  35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.competitor_shares line 201
  36. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.data line 212
  37. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.admissible_covered line 231
  38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.orbits_card_le line 240
  39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.actualCompatible line 247
  40. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.actualUseful line 252
  41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.actualKeep line 258
  42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.actualCompatible_coarse line 262
  43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.actualUseful_coarse line 272
  44. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.competitor_coverage line 282
  45. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.mem_passing line 298
  46. def OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.fullFiber line 318
  47. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.mem_fullFiber line 321
  48. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.mem_fullFiber_mk line 325
  49. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.fullFiber_nonempty line 335
  50. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.fullFiber_card_pos line 340
  51. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.fullFiber_mk line 348
  52. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.fullFiber_eq_orbitSet line 355
  53. def OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.transportedFiber line 362
  54. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.mem_transportedFiber line 366
  55. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.transportedFiber_card line 381
  56. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.transportedFiber_card_pos line 386
  57. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.transportedFiber_mk line 392
  58. theorem OAI.MatrixAllFields.MatrixMultiplication.JointOrbitFibers.transportedFiber_filter_card line 420
  59. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.tag line 464
  60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.full_eq_tagged_fiber line 469
  61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.full_eq_tagged_localOrbit line 487
  62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.full_card_localOrbit line 505
  63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldGroupOrbitData.full_filter_card_localOrbit line 512