OAI/GroupTheory/SimpleOvergroups/MatrixNames.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.Column line 15
  2. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.Name line 16
  3. abbrev OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.Raw line 17
  4. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.columnValue line 19
  5. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.value line 20
  6. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.maximum line 22
  7. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.maximum_le_iff line 24
  8. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.le_maximum line 32
  9. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.columnCost line 35
  10. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.cost line 36
  11. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.entry_cost_le line 39
  12. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.column_entry_cost_le line 45
  13. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.oneName line 48
  14. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.product line 50
  15. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.mulVec line 53
  16. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.value_oneName line 56
  17. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.value_product line 60
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.value_mulVec line 65
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.cost_oneName line 71
  20. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.cost_product_le line 80
  21. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.cost_mulVec_le line 93
  22. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.mem_ball line 105
  23. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.column_mem_ball line 109
  24. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.primrec_maximum line 115
  25. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.primrec_columnCost line 122
  26. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.primrec_cost line 128
  27. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.primrec_product line 133
  28. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.primrec_mulVec line 142
  29. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.columnKey line 149
  30. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.matrixKey line 150
  31. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.columnKey_injective line 154
  32. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.matrixKey_injective line 160
  33. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.partialColumnKey line 165
  34. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.partialMatrixKey line 168
  35. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.partialColumnKey_full line 172
  36. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.partialMatrixKey_full line 184
  37. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.partrec_partialColumnKey line 195
  38. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixNames.partrec_partialMatrixKey line 199