OAI/Algebra/OddKaplansky/OrderedBlocks.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.OrderedOrbitBlock.shift_eq_iff line 20
  2. lemma OAI.OddKaplansky.OrderedOrbitBlock.coset_shift line 88
  3. def OAI.OddKaplansky.OrderedOrbitBlock.unit line 91
  4. lemma OAI.OddKaplansky.OrderedOrbitBlock.unit_mul line 94
  5. def OAI.OddKaplansky.OrderedOrbitBlock.entry line 117
  6. lemma OAI.OddKaplansky.OrderedOrbitBlock.entry_apply line 121
  7. lemma OAI.OddKaplansky.OrderedOrbitBlock.entry_single line 123
  8. lemma OAI.OddKaplansky.OrderedOrbitBlock.entry_mul line 128
  9. def OAI.OddKaplansky.OrderedOrbitBlock.lift line 140
  10. lemma OAI.OddKaplansky.OrderedOrbitBlock.lift_apply line 144
  11. lemma OAI.OddKaplansky.OrderedOrbitBlock.entry_lift line 147
  12. lemma OAI.OddKaplansky.OrderedOrbitBlock.lift_mul line 154
  13. def OAI.OddKaplansky.OrderedOrbitBlock.identity line 164
  14. lemma OAI.OddKaplansky.OrderedOrbitBlock.entry_one line 165
  15. lemma OAI.OddKaplansky.OrderedOrbitBlock.lift_one line 167
  16. lemma OAI.OddKaplansky.OrderedOrbitBlock.unit_cocycle line 169
  17. lemma OAI.OddKaplansky.OrderedOrbitBlock.lift_groupMatrix line 173
  18. lemma OAI.OddKaplansky.OrderedOrbitBlock.lift_representation line 180
  19. lemma OAI.OddKaplansky.OrderedOrbitBlock.unit_cross line 192
  20. lemma OAI.OddKaplansky.OrderedOrbitBlock.entry_cross line 201
  21. lemma OAI.OddKaplansky.OrderedOrbitBlock.lift_cross line 207