OAI/GroupTheory/FiniteType/PrefixPermutation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrefixPermutation.prefix_injective line 16
  2. def OAI.PrefixPermutation.matrixPart line 26
  3. def OAI.PrefixPermutation.support line 28
  4. lemma OAI.PrefixPermutation.partial_one line 31
  5. lemma OAI.PrefixPermutation.partial_mul line 34
  6. lemma OAI.PrefixPermutation.support_mul line 53
  7. lemma OAI.PrefixPermutation.mul_support line 57
  8. lemma OAI.PrefixPermutation.support_idempotent line 61
  9. def OAI.PrefixPermutation.value line 64
  10. lemma OAI.PrefixPermutation.value_one line 67
  11. lemma OAI.PrefixPermutation.value_mul line 70
  12. def OAI.PrefixPermutation.units line 78
  13. lemma OAI.PrefixPermutation.partial_prefix line 88
  14. lemma OAI.PrefixPermutation.value_prefix line 102
  15. lemma OAI.PrefixPermutation.partial_outside line 111
  16. lemma OAI.PrefixPermutation.value_outside line 121
  17. def OAI.NoncommElementary.columnPerm line 132
  18. def OAI.NoncommElementary.columnAction line 138
  19. lemma OAI.NoncommElementary.columnAction_injective line 146
  20. lemma OAI.NoncommElementary.root_mulVec line 153
  21. lemma OAI.NoncommElementary.position_mulVec line 158
  22. def OAI.NoncommElementary.exchange line 165
  23. lemma OAI.NoncommElementary.exchange_mem line 168
  24. lemma OAI.NoncommElementary.exchange_val line 173
  25. lemma OAI.NoncommElementary.exchange_fixes line 182
  26. lemma OAI.NoncommElementary.exchange_move line 187
  27. def OAI.PrefixPermutation.complement line 208
  28. lemma OAI.PrefixPermutation.complement_idempotent line 211
  29. lemma OAI.PrefixPermutation.complement_prefix line 219
  30. lemma OAI.PrefixPermutation.complement_support line 226