OAI/GroupTheory/SimpleOvergroups/DoubleEffective.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.G₀ line 21
  2. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.X₀ line 22
  3. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.G₁ line 23
  4. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.X₁ line 24
  5. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.G₂ line 25
  6. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.X₂ line 26
  7. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.base line 28
  8. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.first line 29
  9. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.operations line 30
  10. def OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partialGroupKey line 36
  11. def OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partialPointKey line 41
  12. def OAI.SimpleFInftyOvergroups.EffectiveNames.Double.test line 46
  13. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.calculus line 54
  14. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.interpret₁ line 62
  15. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Double.interpretation line 65
  16. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partialGroupKey_full line 69
  17. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partialPointKey_full line 82
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.test_full line 95
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_inv_base line 110
  20. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_act_base line 112
  21. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_inv_first line 116
  22. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_plan line 119
  23. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partrec_partialGroupKey line 124
  24. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partrec_partialPointKey line 130
  25. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.partrec_test line 136
  26. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_gcost line 142
  27. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_xcost line 147
  28. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Double.primrec_cost line 153