OAI/Analysis/NuclearUltrapower/IntegerMatrices.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NuclearUltrapower.SOS.genSet line 10
  2. theorem OAI.NuclearUltrapower.SOS.generators_det line 12
  3. theorem OAI.NuclearUltrapower.SOS.generators_inverse line 15
  4. theorem OAI.NuclearUltrapower.SOS.genSet_inv line 18
  5. def OAI.NuclearUltrapower.SOS.GoodWord line 24
  6. theorem OAI.NuclearUltrapower.SOS.goodWord_one line 28
  7. theorem OAI.NuclearUltrapower.SOS.goodWord_generator line 32
  8. theorem OAI.NuclearUltrapower.SOS.goodWord_mul line 39
  9. theorem OAI.NuclearUltrapower.SOS.goodWord_mono line 49
  10. theorem OAI.NuclearUltrapower.SOS.goodWord_inv line 53
  11. def OAI.NuclearUltrapower.SOS.matrixWord line 62
  12. theorem OAI.NuclearUltrapower.SOS.matrixWord_good line 66
  13. def OAI.NuclearUltrapower.SOS.generator0 line 75
  14. def OAI.NuclearUltrapower.SOS.generator1 line 76
  15. def OAI.NuclearUltrapower.SOS.generator2 line 77
  16. def OAI.NuclearUltrapower.SOS.generator3 line 78
  17. def OAI.NuclearUltrapower.SOS.generator4 line 79
  18. def OAI.NuclearUltrapower.SOS.generator5 line 80
  19. def OAI.NuclearUltrapower.SOS.generator6 line 81
  20. def OAI.NuclearUltrapower.SOS.generator7 line 82
  21. def OAI.NuclearUltrapower.SOS.generator8 line 83
  22. def OAI.NuclearUltrapower.SOS.generator9 line 84
  23. def OAI.NuclearUltrapower.SOS.generator10 line 85
  24. def OAI.NuclearUltrapower.SOS.generator11 line 86
  25. def OAI.NuclearUltrapower.SOS.basisWords line 87
  26. theorem OAI.NuclearUltrapower.SOS.basis_words line 88
  27. theorem OAI.NuclearUltrapower.SOS.basisWords_length line 90
  28. theorem OAI.NuclearUltrapower.SOS.basisWords_support line 92
  29. theorem OAI.NuclearUltrapower.SOS.basis_good line 94
  30. def OAI.NuclearUltrapower.SOS.elementary line 109

    Source documentation

    The subgroup generated by the elementary integer matrices.

    def elementary : Subgroup SL := Subgroup.closure (genSet : Set SL)

    Mentions: OAI.NuclearUltrapower.SOS.SL, OAI.NuclearUltrapower.SOS.genSet

  31. abbrev OAI.NuclearUltrapower.SOS.E line 110
  32. def OAI.NuclearUltrapower.SOS.eInterpret line 112
  33. theorem OAI.NuclearUltrapower.SOS.goodWord_mem line 116
  34. theorem OAI.NuclearUltrapower.SOS.eInterpret_coe line 121
  35. theorem OAI.NuclearUltrapower.SOS.eInterpret_one line 125
  36. theorem OAI.NuclearUltrapower.SOS.eInterpret_mul line 130
  37. theorem OAI.NuclearUltrapower.SOS.eInterpret_inv line 137
  38. def OAI.NuclearUltrapower.SOS.eGenSet line 143
  39. theorem OAI.NuclearUltrapower.SOS.mem_eGenSet line 145
  40. theorem OAI.NuclearUltrapower.SOS.eGenSet_inv line 158
  41. theorem OAI.NuclearUltrapower.SOS.eWord line 161
  42. theorem OAI.NuclearUltrapower.SOS.eSet_generates line 178