OAI/GroupTheory/SimpleOvergroups/TruncatedArrays.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayBall line 16
  2. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCollect line 18
  3. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCollect_single line 20
  4. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayBall_zero line 24
  5. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayBall_single line 26
  6. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayBall_add line 31
  7. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayBall_mono line 38
  8. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.array_induction line 41
  9. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrays line 55
  10. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCanonical line 62
  11. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCanonical_single line 65
  12. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCanonical_mem line 69
  13. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCanonical_congr line 75
  14. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.arrayCollect_canonical line 83
  15. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraBall line 96
  16. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraCollect line 98
  17. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraCollect_single line 101
  18. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraBall_zero line 107
  19. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraBall_single line 109
  20. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraBall_add line 114
  21. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebra_induction line 118
  22. def OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraCanonical line 129
  23. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraCanonical_single line 133
  24. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.KeyBall.algebraCanonical_congr line 139
  25. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.algebra_mul_mem line 150
  26. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.algebraCollect_product line 170
  27. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.algebraCollect_mul_congr line 197
  28. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.array_action_mem line 207
  29. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.arrayCollect_action line 230
  30. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.arrayCollect_action_congr line 265
  31. def OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.enlargement line 276
  32. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.unitMap_mem line 309
  33. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.ActionCalculus.basis_mem line 317