OAI/GroupTheory/SimpleOvergroups/EnlargementEffective.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.arrayKey line 19
  2. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.arrayKey_injective line 23
  3. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pairedKey line 26
  4. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pairedKey_injective line 29
  5. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.calculus line 37
  6. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.groupLabel line 43
  7. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pointLabel line 45
  8. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.interpretation line 48
  9. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.partialGroupKey line 62
  10. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.partialPointKey line 66
  11. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.partialGroupKey_full line 70
  12. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.partialPointKey_full line 92
  13. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.computable_array_eq line 103
  14. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_inverse line 113
  15. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_act line 118
  16. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_plan line 123
  17. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_rootArray line 127
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_array line 136
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_pointArray line 142
  20. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_gcost line 149
  21. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.primrec_xcost line 157
  22. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.partrec_partialGroupKey line 165
  23. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.partrec_partialPointKey line 179