OAI/Algebra/OddKaplansky/CosetMatrix.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.CosetMatrix.Q line 14
  2. abbrev OAI.OddKaplansky.CosetMatrix.D line 15
  3. lemma OAI.OddKaplansky.CosetMatrix.mk_left line 17
  4. lemma OAI.OddKaplansky.CosetMatrix.mk_mul_rep line 22
  5. def OAI.OddKaplansky.CosetMatrix.cocycle line 23
  6. lemma OAI.OddKaplansky.CosetMatrix.cocycle_reconstruct line 24
  7. lemma OAI.OddKaplansky.CosetMatrix.cocycle_one line 26
  8. lemma OAI.OddKaplansky.CosetMatrix.cocycle_mul line 33
  9. def OAI.OddKaplansky.CosetMatrix.groupMatrix line 39
  10. lemma OAI.OddKaplansky.CosetMatrix.groupMatrix_one line 41
  11. lemma OAI.OddKaplansky.CosetMatrix.groupMatrix_mul line 44
  12. def OAI.OddKaplansky.CosetMatrix.representation line 51
  13. lemma OAI.OddKaplansky.CosetMatrix.representation_single line 53
  14. def OAI.OddKaplansky.CosetMatrix.coefficients line 56
  15. def OAI.OddKaplansky.CosetMatrix.unpack line 58
  16. lemma OAI.OddKaplansky.CosetMatrix.unpack_coeff line 62
  17. lemma OAI.OddKaplansky.CosetMatrix.unpack_symm_coeff line 64
  18. lemma OAI.OddKaplansky.CosetMatrix.unpack_basis line 69
  19. lemma OAI.OddKaplansky.CosetMatrix.residue_left line 86
  20. lemma OAI.OddKaplansky.CosetMatrix.groupMatrix_mulVec line 90
  21. lemma OAI.OddKaplansky.CosetMatrix.unpack_group line 101
  22. lemma OAI.OddKaplansky.CosetMatrix.unpack_representation line 111
  23. def OAI.OddKaplansky.CosetMatrix.endomorphism line 121
  24. lemma OAI.OddKaplansky.CosetMatrix.endomorphism_idempotent line 123
  25. lemma OAI.OddKaplansky.CosetMatrix.endomorphism_rank line 127