OAI/Algebra/AuslanderReiten/Stable/StableHom.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.FactorsThroughFiniteFree line 17
  2. def OAI.ArExplicit.FactorsThroughFiniteProjective line 22
  3. theorem OAI.ArExplicit.factorsThroughFiniteFree_iff_projective line 29
  4. theorem OAI.ArExplicit.factorsThroughFiniteFree_zero line 44
  5. theorem OAI.ArExplicit.FactorsThroughFiniteFree.add line 48
  6. theorem OAI.ArExplicit.FactorsThroughFiniteFree.neg line 58
  7. theorem OAI.ArExplicit.FactorsThroughFiniteFree.postcomp line 68
  8. theorem OAI.ArExplicit.FactorsThroughFiniteFree.precomp line 74
  9. def OAI.ArExplicit.projectiveMaps line 82
  10. abbrev OAI.ArExplicit.StableHom line 88
  11. def OAI.ArExplicit.StableHom.classOf line 92
  12. theorem OAI.ArExplicit.StableHom.classOf_surjective line 97
  13. theorem OAI.ArExplicit.StableHom.classOf_eq_zero_iff line 101
  14. theorem OAI.ArExplicit.StableHom.classOf_eq_zero_iff_projective line 105
  15. theorem OAI.ArExplicit.StableHom.classOf_eq_iff line 110
  16. theorem OAI.ArExplicit.StableHom.identity_eq_zero_iff line 114
  17. def OAI.ArExplicit.StableHom.postcomp line 124
  18. def OAI.ArExplicit.StableHom.precomp line 131
  19. theorem OAI.ArExplicit.StableHom.postcomp_classOf line 139
  20. theorem OAI.ArExplicit.StableHom.precomp_classOf line 144
  21. def OAI.ArExplicit.StableHom.postcompHom line 148
  22. def OAI.ArExplicit.StableHom.comp line 164
  23. theorem OAI.ArExplicit.StableHom.comp_classOf line 174
  24. def OAI.ArExplicit.StableHom.identity line 179
  25. theorem OAI.ArExplicit.StableHom.identity_comp line 182
  26. theorem OAI.ArExplicit.StableHom.comp_identity line 187
  27. theorem OAI.ArExplicit.StableHom.comp_assoc line 191
  28. theorem OAI.ArExplicit.StableHom.eq_zero_of_projective_source line 199
  29. theorem OAI.ArExplicit.StableHom.eq_zero_of_projective_target line 206
  30. theorem OAI.ArExplicit.FactorsThroughFiniteFree.smul line 221
  31. def OAI.ArExplicit.projectiveMapsSubmodule line 229
  32. instance OAI.ArExplicit.stableHomModule line 233
  33. def OAI.ArExplicit.StableHom.classOfLinear line 238
  34. theorem OAI.ArExplicit.StableHom.classOfLinear_apply line 242
  35. theorem OAI.ArExplicit.StableHom.classOf_smul line 246
  36. theorem OAI.ArExplicit.StableHom.comp_smul line 252
  37. theorem OAI.ArExplicit.StableHom.smul_comp line 260
  38. def OAI.ArExplicit.StableHom.postcompLinear line 267
  39. def OAI.ArExplicit.StableHom.compLinear line 273
  40. theorem OAI.ArExplicit.StableHom.compLinear_apply line 289