OAI/Algebra/OddKaplansky/GreedyRing.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.GreedyRing.Eā‚€ line 17
  2. lemma OAI.OddKaplansky.GreedyRing.Eā‚€_idem line 18
  3. abbrev OAI.OddKaplansky.GreedyRing.I line 46
  4. abbrev OAI.OddKaplansky.GreedyRing.J line 47
  5. def OAI.OddKaplansky.GreedyRing.columns line 48
  6. def OAI.OddKaplansky.GreedyRing.indices line 49
  7. def OAI.OddKaplansky.GreedyRing.Q line 51
  8. lemma OAI.OddKaplansky.GreedyRing.Q_map line 52
  9. lemma OAI.OddKaplansky.GreedyRing.Q_det_unit line 62
  10. def OAI.OddKaplansky.GreedyRing.equiv line 68
  11. lemma OAI.OddKaplansky.GreedyRing.equiv_apply line 71
  12. lemma OAI.OddKaplansky.GreedyRing.equiv_symm_apply line 72
  13. def OAI.OddKaplansky.GreedyRing.basis line 74
  14. lemma OAI.OddKaplansky.GreedyRing.basis_apply line 76
  15. lemma OAI.OddKaplansky.GreedyRing.basis_inl line 81
  16. lemma OAI.OddKaplansky.GreedyRing.basis_inr line 82
  17. lemma OAI.OddKaplansky.GreedyRing.fixed_inl line 83
  18. lemma OAI.OddKaplansky.GreedyRing.killed_inr line 87
  19. lemma OAI.OddKaplansky.GreedyRing.image_independent line 92
  20. lemma OAI.OddKaplansky.GreedyRing.image_span line 94
  21. def OAI.OddKaplansky.GreedyRing.imageBasis line 106
  22. lemma OAI.OddKaplansky.GreedyRing.imageBasis_apply line 108