OAI/GroupTheory/SimpleOvergroups/MatrixEffective.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleFInftyOvergroups.BoundedEncoding.WithBound.ext' line 9
  2. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.pairedKey line 22
  3. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.pairedKey_injective line 26
  4. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.calculus line 31
  5. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.groupLabel line 34
  6. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.pointLabel line 37
  7. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.interpretation line 40
  8. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.partialGroupKey line 53
  9. def OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.partialPointKey line 58
  10. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.partialGroupKey_full line 61
  11. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.partialPointKey_full line 75
  12. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_rootInv line 85
  13. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_inverse line 89
  14. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_rootMatrix line 93
  15. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_matrix line 104
  16. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_column line 109
  17. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_gcost line 113
  18. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.primrec_xcost line 122
  19. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.partrec_partialGroupKey line 128
  20. theorem OAI.SimpleFInftyOvergroups.EffectiveNames.MatrixWords.partrec_partialPointKey line 139