OAI/GroupTheory/SimpleOvergroups/SemanticEnlargements.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.IdempotentNames.Index line 14
  2. instance OAI.SimpleFInftyOvergroups.SemanticEncoding.IdempotentNames.(instance at line 15) line 15
  3. instance OAI.SimpleFInftyOvergroups.SemanticEncoding.IdempotentNames.(instance at line 17) line 17
  4. def OAI.SimpleFInftyOvergroups.SemanticEncoding.IdempotentNames.name line 21
  5. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.IdempotentNames.value_name line 23
  6. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.IdempotentNames.idempotent line 25
  7. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.Word line 40
  8. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.Point line 41
  9. abbrev OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.ambient line 43
  10. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.calculus line 45
  11. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.group_mem line 60
  12. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupValue line 70
  13. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.pointValue line 72
  14. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupValue_nil line 76
  15. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupValue_append line 78
  16. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupValue_inverse line 83
  17. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupValue_singleton line 88
  18. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.pointValue_act line 96
  19. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.pointValue_basis line 100
  20. def OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.interpretation line 105
  21. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupKey_injective line 119
  22. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.pointKey_injective line 128
  23. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.groupValue_surjective line 134
  24. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.partialGroupKey_full line 152
  25. theorem OAI.SimpleFInftyOvergroups.SemanticEncoding.SemanticEnlargement.partialPointKey_full line 158