OAI/Algebra/OddKaplansky/SectorOrbit.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.SectorOrbit.action line 15
  2. abbrev OAI.OddKaplansky.SectorOrbit.Rep line 20
  3. def OAI.OddKaplansky.SectorOrbit.lmb line 21
  4. lemma OAI.OddKaplansky.SectorOrbit.lmb_weight line 22
  5. def OAI.OddKaplansky.SectorOrbit.T line 23
  6. lemma OAI.OddKaplansky.SectorOrbit.mem_T line 24
  7. lemma OAI.OddKaplansky.SectorOrbit.separate line 25
  8. def OAI.OddKaplansky.SectorOrbit.orbitMap line 32
  9. lemma OAI.OddKaplansky.SectorOrbit.orbitMap_injective line 35
  10. lemma OAI.OddKaplansky.SectorOrbit.orbitMap_surjective line 47
  11. def OAI.OddKaplansky.SectorOrbit.orbitEquiv line 56
  12. lemma OAI.OddKaplansky.SectorOrbit.identity_sum line 59
  13. abbrev OAI.OddKaplansky.SectorOrbit.Block line 68
  14. def OAI.OddKaplansky.SectorOrbit.pack line 69
  15. lemma OAI.OddKaplansky.SectorOrbit.pack_apply line 73
  16. lemma OAI.OddKaplansky.SectorOrbit.pack_mul line 76
  17. lemma OAI.OddKaplansky.SectorOrbit.pack_one line 87
  18. lemma OAI.OddKaplansky.SectorOrbit.pack_representation line 92