OAI/Algebra/OddKaplansky/AugmentationMatrices.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.Augmentation.High line 17
  2. def OAI.OddKaplansky.Augmentation.columns line 19
  3. def OAI.OddKaplansky.Augmentation.regular line 22
  4. lemma OAI.OddKaplansky.Augmentation.basis_repr line 25
  5. lemma OAI.OddKaplansky.Augmentation.regular_delta line 39
  6. lemma OAI.OddKaplansky.Augmentation.regular_mul_vec line 58
  7. lemma OAI.OddKaplansky.Augmentation.columns_independent line 74
  8. lemma OAI.OddKaplansky.Augmentation.columns_annihilated line 80
  9. lemma OAI.OddKaplansky.Augmentation.regular_delta_transpose line 89
  10. lemma OAI.OddKaplansky.Augmentation.columns_transpose_annihilated line 99