OAI/Algebra/OddKaplansky/OrderedOrbits.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.OrderedSectorOrbit.action line 16
  2. abbrev OAI.OddKaplansky.OrderedSectorOrbit.Rep line 21
  3. def OAI.OddKaplansky.OrderedSectorOrbit.characterOrder line 23
  4. def OAI.OddKaplansky.OrderedSectorOrbit.lmb line 24
  5. lemma OAI.OddKaplansky.OrderedSectorOrbit.lmb_spec line 25
  6. lemma OAI.OddKaplansky.OrderedSectorOrbit.cover line 28
  7. lemma OAI.OddKaplansky.OrderedSectorOrbit.lmb_weight line 33
  8. def OAI.OddKaplansky.OrderedSectorOrbit.T line 34
  9. lemma OAI.OddKaplansky.OrderedSectorOrbit.mem_T line 35
  10. lemma OAI.OddKaplansky.OrderedSectorOrbit.separate line 36
  11. def OAI.OddKaplansky.OrderedSectorOrbit.orbitMap line 43
  12. lemma OAI.OddKaplansky.OrderedSectorOrbit.orbitMap_injective line 46
  13. lemma OAI.OddKaplansky.OrderedSectorOrbit.orbitMap_surjective line 58
  14. def OAI.OddKaplansky.OrderedSectorOrbit.orbitEquiv line 67
  15. lemma OAI.OddKaplansky.OrderedSectorOrbit.identity_sum line 70
  16. abbrev OAI.OddKaplansky.OrderedSectorOrbit.Block line 79
  17. def OAI.OddKaplansky.OrderedSectorOrbit.pack line 80
  18. lemma OAI.OddKaplansky.OrderedSectorOrbit.pack_apply line 84
  19. lemma OAI.OddKaplansky.OrderedSectorOrbit.pack_mul line 87
  20. lemma OAI.OddKaplansky.OrderedSectorOrbit.pack_one line 98
  21. lemma OAI.OddKaplansky.OrderedSectorOrbit.pack_representation line 103