OAI/Algebra/OddKaplansky/SectorStabilizer.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.SectorStabilizer.stabilizer line 12
  2. abbrev OAI.OddKaplansky.SectorStabilizer.Point line 18
  3. abbrev OAI.OddKaplansky.SectorStabilizer.H line 19
  4. instance OAI.OddKaplansky.SectorStabilizer.(instance at line 20) line 20
  5. def OAI.OddKaplansky.SectorStabilizer.baseHom line 21
  6. lemma OAI.OddKaplansky.SectorStabilizer.base_pow line 25
  7. lemma OAI.OddKaplansky.SectorStabilizer.pow_of_right line 33
  8. def OAI.OddKaplansky.SectorStabilizer.toPoint line 37
  9. lemma OAI.OddKaplansky.SectorStabilizer.toPoint_kernel line 39
  10. lemma OAI.OddKaplansky.SectorStabilizer.toPoint_injective line 43
  11. lemma OAI.OddKaplansky.SectorStabilizer.commutative line 48
  12. def OAI.OddKaplansky.SectorStabilizer.commGroup line 52
  13. lemma OAI.OddKaplansky.SectorStabilizer.exponent line 55