OAI/Algebra/OddKaplansky/OrderedMatrices.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.OrderedCosetMatrix.Q line 15
  2. abbrev OAI.OddKaplansky.OrderedCosetMatrix.D line 16
  3. lemma OAI.OddKaplansky.OrderedCosetMatrix.mk_left line 18
  4. lemma OAI.OddKaplansky.OrderedCosetMatrix.mk_mul_rep line 24
  5. def OAI.OddKaplansky.OrderedCosetMatrix.cocycle line 25
  6. lemma OAI.OddKaplansky.OrderedCosetMatrix.cocycle_reconstruct line 26
  7. lemma OAI.OddKaplansky.OrderedCosetMatrix.cocycle_one line 28
  8. lemma OAI.OddKaplansky.OrderedCosetMatrix.cocycle_mul line 31
  9. def OAI.OddKaplansky.OrderedCosetMatrix.groupMatrix line 37
  10. lemma OAI.OddKaplansky.OrderedCosetMatrix.groupMatrix_one line 39
  11. lemma OAI.OddKaplansky.OrderedCosetMatrix.groupMatrix_mul line 42
  12. def OAI.OddKaplansky.OrderedCosetMatrix.representation line 49
  13. lemma OAI.OddKaplansky.OrderedCosetMatrix.representation_single line 51
  14. def OAI.OddKaplansky.OrderedCosetMatrix.coefficients line 54
  15. def OAI.OddKaplansky.OrderedCosetMatrix.unpack line 56
  16. lemma OAI.OddKaplansky.OrderedCosetMatrix.unpack_coeff line 60
  17. lemma OAI.OddKaplansky.OrderedCosetMatrix.unpack_symm_coeff line 62
  18. lemma OAI.OddKaplansky.OrderedCosetMatrix.unpack_basis line 67
  19. lemma OAI.OddKaplansky.OrderedCosetMatrix.residue_left line 84
  20. lemma OAI.OddKaplansky.OrderedCosetMatrix.groupMatrix_mulVec line 88
  21. lemma OAI.OddKaplansky.OrderedCosetMatrix.unpack_group line 99
  22. lemma OAI.OddKaplansky.OrderedCosetMatrix.unpack_representation line 109
  23. def OAI.OddKaplansky.OrderedCosetMatrix.endomorphism line 119
  24. lemma OAI.OddKaplansky.OrderedCosetMatrix.endomorphism_idempotent line 121
  25. lemma OAI.OddKaplansky.OrderedCosetMatrix.endomorphism_rank line 125