OAI/GroupTheory/SimpleOvergroups/MatrixWords.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.Root line 15
  2. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.Word line 16
  3. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.Point line 17
  4. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.V line 18
  5. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.rootInv line 20
  6. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.inverse line 21
  7. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.rootValue line 23
  8. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupValue line 27
  9. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupValue_nil line 29
  10. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupValue_cons line 30
  11. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupValue_append line 32
  12. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.rootValue_inv line 35
  13. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.inverse_nil line 44
  14. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.inverse_cons line 45
  15. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupValue_inverse line 48
  16. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.gcost line 53
  17. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.xcost line 56
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.gcost_nil line 60
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.gcost_cons line 62
  20. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.gcost_append line 65
  21. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.gcost_inverse line 67
  22. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.nameOperations line 71
  23. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.pointValue line 85
  24. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.pointValue_act line 87
  25. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.rootMatrix line 91
  26. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.matrix line 94
  27. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.column line 96
  28. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.value_rootMatrix line 98
  29. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.value_matrix line 114
  30. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.value_column line 121
  31. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.cost_rootMatrix line 125
  32. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.cost_matrix line 139
  33. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.cost_column line 149
  34. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.grade line 157
  35. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.grade_nil line 159
  36. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.grade_append line 160
  37. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupValue_mem line 162
  38. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.pointValue_mem line 173