OAI/RingTheory/BassTrace/RightRetractions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BassTrace.RightProjective.unopTranspose_mul line 19
  2. lemma OAI.BassTrace.RightProjective.rightMatrix_comp line 28
  3. lemma OAI.BassTrace.RightProjective.Retraction.exists_ line 37
  4. lemma OAI.BassTrace.RightProjective.classOf_eq_of_rectangular line 42
  5. lemma OAI.BassTrace.RightProjective.Retraction.class_eq line 54
  6. lemma OAI.BassTrace.RightProjective.Retraction.transport_idempotent line 73
  7. lemma OAI.BassTrace.RightProjective.freeSplit_apply_left line 93
  8. lemma OAI.BassTrace.RightProjective.freeSplit_apply_right line 96
  9. lemma OAI.BassTrace.RightProjective.freeSplit_symm_left line 99
  10. lemma OAI.BassTrace.RightProjective.freeSplit_symm_right line 104
  11. lemma OAI.BassTrace.RightProjective.freeSplit_single_left line 109
  12. lemma OAI.BassTrace.RightProjective.freeSplit_single_right line 119
  13. lemma OAI.BassTrace.RightProjective.rightMatrix_apply line 132
  14. lemma OAI.BassTrace.RightProjective.Retraction.prod_matrix line 136
  15. lemma OAI.BassTrace.RightProjective.Retraction.prod_idempotent line 162
  16. lemma OAI.BassTrace.RightProjective.classOf_directSum line 168