OAI/GroupTheory/SimpleOvergroups/TruncatedAction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall line 11
  2. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.Represented line 19
  3. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.leastCost line 21
  4. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.leastCost_spec line 24
  5. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.represented_key line 29
  6. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.leastCost_le line 32
  7. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.representative line 39
  8. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.representative_spec line 43
  9. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.canonical line 50
  10. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.canonical_congr line 52
  11. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.canonical_mem line 55
  12. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.key_canonical line 60
  13. structure OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus line 66
  14. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.inverse_action_iff line 89
  15. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.inverse_action_iff_of_total line 101
  16. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.group_context line 107
  17. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.rawMatrixAction line 121
  18. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixCollect_product line 128
  19. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.columnCollect_product line 134
  20. def OAI.SimpleFInftyOvergroups.BoundedEncoding.WordCalculus.matrixActionCalculus line 141