OAI/Algebra/OddKaplansky/SectorGroup.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.SectorGroup.Attached line 12
  2. abbrev OAI.OddKaplansky.SectorGroup.Common line 13
  3. def OAI.OddKaplansky.SectorGroup.toBase line 14
  4. def OAI.OddKaplansky.SectorGroup.toAttached line 16
  5. lemma OAI.OddKaplansky.SectorGroup.toBase_injective line 20
  6. lemma OAI.OddKaplansky.SectorGroup.toAttached_injective line 39
  7. abbrev OAI.OddKaplansky.SectorGroup.Gā‚ line 49
  8. def OAI.OddKaplansky.SectorGroup.base line 50
  9. def OAI.OddKaplansky.SectorGroup.factor line 51
  10. def OAI.OddKaplansky.SectorGroup.original line 52
  11. def OAI.OddKaplansky.SectorGroup.central line 53
  12. lemma OAI.OddKaplansky.SectorGroup.base_injective line 54
  13. lemma OAI.OddKaplansky.SectorGroup.factor_injective line 56
  14. lemma OAI.OddKaplansky.SectorGroup.original_injective line 58
  15. lemma OAI.OddKaplansky.SectorGroup.central_injective line 61
  16. lemma OAI.OddKaplansky.SectorGroup.identify_top line 64
  17. lemma OAI.OddKaplansky.SectorGroup.identify_diagonal line 81
  18. lemma OAI.OddKaplansky.SectorGroup.central_commute line 98
  19. instance OAI.OddKaplansky.SectorGroup.(instance at line 118) line 118
  20. def OAI.OddKaplansky.SectorGroup.f line 120
  21. lemma OAI.OddKaplansky.SectorGroup.f_idempotent line 121
  22. lemma OAI.OddKaplansky.SectorGroup.f_ne_zero line 142
  23. lemma OAI.OddKaplansky.SectorGroup.f_central line 144
  24. lemma OAI.OddKaplansky.SectorGroup.factor_f line 146
  25. lemma OAI.OddKaplansky.SectorGroup.factor_original line 150