OAI/GroupTheory/SimpleOvergroups/TruncatedMatrix.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.MatrixBall line 18
  2. abbrev OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.ColumnBall line 20
  3. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect line 22
  4. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect line 24
  5. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_apply line 27
  6. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_apply line 30
  7. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_one line 34
  8. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_zero line 37
  9. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_zero line 40
  10. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixBall_one line 44
  11. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixBall_zero line 48
  12. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnBall_zero line 51
  13. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixBall_add line 55
  14. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixBall_sub line 59
  15. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixBall_single line 64
  16. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixBall_mul line 70
  17. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnBall_mulVec line 77
  18. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_mem line 84
  19. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_mem line 89
  20. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_idempotent line 94
  21. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_idempotent line 100
  22. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_mul_left line 106
  23. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_mul_right line 116
  24. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_context line 126
  25. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_mulVec_left line 138
  26. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_mulVec_right line 149
  27. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_context line 160
  28. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixPair line 168
  29. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.UnitBall line 171
  30. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.unitBall_one line 174
  31. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.unitBall_inv line 178
  32. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.unitBall_mul line 181
  33. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.unitBall_elementary line 187
  34. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixPair_context line 193
  35. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixPair_inv line 207
  36. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixPair_action line 211
  37. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.inverse_action_iff line 220
  38. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.inverse_action_iff_of_total line 236