OAI/Algebra/OddKaplansky/GreedyLift.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.GreedyLift.I line 14
  2. abbrev OAI.OddKaplansky.GreedyLift.J line 15
  3. def OAI.OddKaplansky.GreedyLift.columns line 16
  4. lemma OAI.OddKaplansky.GreedyLift.complement line 18
  5. lemma OAI.OddKaplansky.GreedyLift.independent line 28
  6. lemma OAI.OddKaplansky.GreedyLift.spanning line 33
  7. def OAI.OddKaplansky.GreedyLift.basis line 37
  8. lemma OAI.OddKaplansky.GreedyLift.card_indices line 40
  9. def OAI.OddKaplansky.GreedyLift.indices line 44
  10. def OAI.OddKaplansky.GreedyLift.matrix line 47
  11. lemma OAI.OddKaplansky.GreedyLift.matrix_independent line 48
  12. lemma OAI.OddKaplansky.GreedyLift.matrix_det line 50