OAI/Algebra/OddKaplansky/Compression.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OddKaplansky.Compression.nilpotent_lower line 15
  2. def OAI.OddKaplansky.Compression.C₀ line 34
  3. def OAI.OddKaplansky.Compression.D₀ line 35
  4. lemma OAI.OddKaplansky.Compression.D₀C₀ line 36
  5. lemma OAI.OddKaplansky.Compression.diag_idempotent line 49
  6. lemma OAI.OddKaplansky.Compression.C₀_diag line 55
  7. lemma OAI.OddKaplansky.Compression.diag_D₀ line 69
  8. def OAI.OddKaplansky.Compression.error line 84
  9. def OAI.OddKaplansky.Compression.correction line 85
  10. def OAI.OddKaplansky.Compression.D₁ line 87
  11. lemma OAI.OddKaplansky.Compression.corrected line 88
  12. def OAI.OddKaplansky.Compression.rep line 128
  13. lemma OAI.OddKaplansky.Compression.rep_mul line 129
  14. def OAI.OddKaplansky.Compression.blockJ line 137
  15. def OAI.OddKaplansky.Compression.blockY line 138
  16. lemma OAI.OddKaplansky.Compression.blockYJ line 139
  17. lemma OAI.OddKaplansky.Compression.blockJY line 156
  18. def OAI.OddKaplansky.Compression.Csharp line 173
  19. def OAI.OddKaplansky.Compression.Dsharp line 175
  20. lemma OAI.OddKaplansky.Compression.compressed line 177
  21. lemma OAI.OddKaplansky.Compression.Csharp_sector line 197
  22. lemma OAI.OddKaplansky.Compression.Dsharp_sector line 221