OAI/Algebra/OddKaplansky/OrbitBlock.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.OrbitBlock.shift_eq_iff line 18
  2. lemma OAI.OddKaplansky.OrbitBlock.coset_shift line 28
  3. def OAI.OddKaplansky.OrbitBlock.unit line 31
  4. lemma OAI.OddKaplansky.OrbitBlock.unit_mul line 34
  5. def OAI.OddKaplansky.OrbitBlock.entry line 57
  6. lemma OAI.OddKaplansky.OrbitBlock.entry_apply line 61
  7. lemma OAI.OddKaplansky.OrbitBlock.entry_single line 63
  8. lemma OAI.OddKaplansky.OrbitBlock.entry_mul line 68
  9. def OAI.OddKaplansky.OrbitBlock.lift line 80
  10. lemma OAI.OddKaplansky.OrbitBlock.lift_apply line 84
  11. lemma OAI.OddKaplansky.OrbitBlock.entry_lift line 87
  12. lemma OAI.OddKaplansky.OrbitBlock.lift_mul line 94
  13. def OAI.OddKaplansky.OrbitBlock.identity line 104
  14. lemma OAI.OddKaplansky.OrbitBlock.entry_one line 105
  15. lemma OAI.OddKaplansky.OrbitBlock.lift_one line 107
  16. lemma OAI.OddKaplansky.OrbitBlock.unit_cocycle line 109
  17. lemma OAI.OddKaplansky.OrbitBlock.lift_groupMatrix line 113
  18. lemma OAI.OddKaplansky.OrbitBlock.lift_representation line 120
  19. lemma OAI.OddKaplansky.OrbitBlock.unit_cross line 132
  20. lemma OAI.OddKaplansky.OrbitBlock.entry_cross line 141
  21. lemma OAI.OddKaplansky.OrbitBlock.lift_cross line 147