OAI/GroupTheory/SimpleOvergroups/EnlargementNames.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.Name line 15
  2. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.value line 17
  3. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.one line 18
  4. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.mul line 19
  5. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.complement line 20
  6. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.value_one line 21
  7. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.value_mul line 22
  8. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Coeff.value_complement line 23
  9. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Word line 29
  10. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.Point line 30
  11. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.rootInv line 32
  12. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.inverse line 33
  13. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.gcost line 34
  14. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.xcost line 35
  15. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.inverse_nil line 36
  16. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.inverse_cons line 37
  17. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.gcost_nil line 39
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.gcost_cons line 40
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.gcost_append line 42
  20. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.gcost_inverse line 43
  21. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.operations line 46
  22. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.rootArray line 60
  23. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.array line 63
  24. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pointArray line 66
  25. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.rootArray_bound line 69
  26. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.array_bound line 76
  27. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pointArray_bound line 84
  28. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.D line 94
  29. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.rootValue line 96
  30. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.groupValue line 99
  31. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.groupValue_nil line 102
  32. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.groupValue_cons line 104
  33. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.groupValue_append line 107
  34. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.rootValue_inv line 111
  35. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.groupValue_inverse line 117
  36. def OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pointValue line 123
  37. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.pointValue_act line 127
  38. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.value_rootArray line 134
  39. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.value_array line 141
  40. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.value_pointArray line 154
  41. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.group_mem line 162
  42. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.Enlargement.point_mem line 171