OAI/RepresentationTheory/UniversalSquare/Contraction/VectorDomainsCore.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Vector Domains Core.

  1. def OAI.Saxl.Columns.permVector line 14
  2. lemma OAI.Saxl.Columns.permVector_get line 16
  3. lemma OAI.Saxl.Columns.permVector_injective line 20
  4. lemma OAI.Saxl.Columns.ofFn_fin_val line 26
  5. lemma OAI.Saxl.Columns.permVector_perm line 31
  6. lemma OAI.Saxl.Columns.permVector_surj line 35
  7. def OAI.Saxl.Columns.vectorFull line 48
  8. lemma OAI.Saxl.Columns.vectorFull_eq_image line 52
  9. def OAI.Saxl.Columns.vectorSign line 61
  10. lemma OAI.Saxl.Columns.sign_eq_aux line 65
  11. lemma OAI.Saxl.Columns.vectorSign_perm line 73
  12. def OAI.Saxl.Columns.VectorDomains line 82
  13. def OAI.Saxl.Columns.VectorDomains.full line 86
  14. def OAI.Saxl.Columns.VectorDomains.atValue line 90
  15. def OAI.Saxl.Columns.VectorDomains.vanished line 94
  16. def OAI.Saxl.Columns.VectorDomains.mass line 98
  17. def OAI.Saxl.Columns.Domains.encode line 102
  18. lemma OAI.Saxl.Columns.Domains.encode_full line 106
  19. lemma OAI.Saxl.Columns.Domains.encode_atValue line 111
  20. lemma OAI.Saxl.Columns.Domains.encode_vanished line 121
  21. lemma OAI.Saxl.Columns.Domains.encode_mass line 128
  22. def OAI.Saxl.Columns.vectorEdgeOptions line 140
  23. lemma OAI.Saxl.Columns.vectorEdgeOptions_encode line 146
  24. def OAI.Saxl.Columns.vectorOrderEdges line 152
  25. lemma OAI.Saxl.Columns.vectorOrderEdges_encode line 157
  26. def OAI.Saxl.Columns.solveVectors line 163
  27. lemma OAI.Saxl.Columns.solveVectors_encode line 175
  28. lemma OAI.Saxl.Columns.contractionInteger_vectors line 194