OAI/GroupTheory/SimpleOvergroups/SemanticActions.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.SemanticEncoding.globalCalculus line 14
  2. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.Raw line 29
  3. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.seven line 31
  4. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.matrixMap line 36
  5. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.matrixMap_apply line 39
  6. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.columnMap line 42
  7. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.matrixMap_mulVec line 44
  8. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.rootValue line 50
  9. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue line 56
  10. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.pointValue line 58
  11. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.rootValue_inverse line 60
  12. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue_nil line 67
  13. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue_append line 68
  14. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue_cons line 70
  15. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue_inverse line 72
  16. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.pointValue_act line 78
  17. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.rootValue_matrix line 84
  18. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue_matrix line 97
  19. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.pointValue_column line 105
  20. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupValue_surjective line 111
  21. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.pointValue_surjective line 130
  22. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupKey line 147
  23. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.pointKey line 151
  24. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.groupKey_injective line 155
  25. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.pointKey_injective line 165
  26. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.calculus line 172
  27. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.interpretation line 175
  28. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.gkey_eq line 189
  29. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.xkey_eq line 208
  30. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.partialGroupKey_full line 219
  31. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticMatrix.partialPointKey_full line 228