OAI/GroupTheory/UniversalGroup/Markers.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Higman.DecoratedMarker.Kernel line 12
  2. abbrev OAI.Higman.DecoratedMarker.Base line 14
  3. def OAI.Higman.DecoratedMarker.shift line 17
  4. theorem OAI.Higman.DecoratedMarker.shift_inl line 21
  5. theorem OAI.Higman.DecoratedMarker.shift_inr_of line 22
  6. def OAI.Higman.DecoratedMarker.shifts line 25
  7. abbrev OAI.Higman.DecoratedMarker.ShiftGroup line 46
  8. def OAI.Higman.DecoratedMarker.coefficient line 49
  9. def OAI.Higman.DecoratedMarker.translation line 50
  10. def OAI.Higman.DecoratedMarker.marker line 51
  11. def OAI.Higman.DecoratedMarker.inclusion line 54
  12. theorem OAI.Higman.DecoratedMarker.inclusion_inl line 57
  13. theorem OAI.Higman.DecoratedMarker.inclusion_inr_of line 59
  14. lemma OAI.Higman.DecoratedMarker.commute_coefficient_translation line 63
  15. lemma OAI.Higman.DecoratedMarker.test_commute line 67
  16. def OAI.Higman.DecoratedMarker.test line 77
  17. theorem OAI.Higman.DecoratedMarker.test_coefficient line 82
  18. theorem OAI.Higman.DecoratedMarker.test_translation line 84
  19. theorem OAI.Higman.DecoratedMarker.test_inr_of line 86
  20. theorem OAI.Higman.DecoratedMarker.test_marker line 88
  21. theorem OAI.Higman.DecoratedMarker.test_comp line 95
  22. theorem OAI.Higman.DecoratedMarker.inclusion_injective line 105
  23. lemma OAI.Higman.DecoratedMarker.inclusion_shift line 110
  24. def OAI.Higman.DecoratedMarker.inverse line 125
  25. theorem OAI.Higman.DecoratedMarker.inverse_inl line 128
  26. theorem OAI.Higman.DecoratedMarker.inverse_inr line 130
  27. theorem OAI.Higman.DecoratedMarker.inverse_comp_test line 133
  28. theorem OAI.Higman.DecoratedMarker.test_comp_inverse line 149
  29. def OAI.Higman.DecoratedMarker.decomposition line 160
  30. def OAI.Higman.DecoratedFreeBasis.inclusion line 169
  31. theorem OAI.Higman.DecoratedFreeBasis.inclusion_of line 172
  32. theorem OAI.Higman.DecoratedFreeBasis.projection_comp line 176
  33. theorem OAI.Higman.DecoratedFreeBasis.inclusion_injective line 182
  34. def OAI.Higman.DecoratedFreeBasis.twist line 187
  35. theorem OAI.Higman.DecoratedFreeBasis.twist_inl line 208
  36. theorem OAI.Higman.DecoratedFreeBasis.twist_inr_of line 210
  37. def OAI.Higman.MarkerEmbedding.index line 220
  38. def OAI.Higman.MarkerEmbedding.kernelMap line 223
  39. theorem OAI.Higman.MarkerEmbedding.kernelMap_inl line 228
  40. theorem OAI.Higman.MarkerEmbedding.kernelMap_inr_of line 230
  41. lemma OAI.Higman.MarkerEmbedding.kernelMap_shift line 234
  42. def OAI.Higman.MarkerEmbedding.embedding line 245
  43. theorem OAI.Higman.MarkerEmbedding.embedding_coefficient line 250
  44. theorem OAI.Higman.MarkerEmbedding.embedding_translation line 253
  45. theorem OAI.Higman.MarkerEmbedding.embedding_inr_of line 256
  46. theorem OAI.Higman.MarkerEmbedding.embedding_marker line 259
  47. theorem OAI.Higman.MarkerEmbedding.kernelMap_injective line 265
  48. theorem OAI.Higman.MarkerEmbedding.embedding_injective line 296
  49. theorem OAI.Higman.MarkerEmbedding.index_injective line 309