OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorHomComplex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.ExternalTensor.homCochain line 17
  2. theorem OAI.ArExplicit.ExternalTensor.homCochain_d line 32
  3. instance OAI.ArExplicit.ExternalTensor.hasHomCochainTotal line 43
  4. abbrev OAI.ArExplicit.ExternalTensor.homCochainTotal line 46
  5. def OAI.ArExplicit.ExternalTensor.homOutTerm line 50
  6. theorem OAI.ArExplicit.ExternalTensor.homOutTerm_bijective line 57
  7. def OAI.ArExplicit.ExternalTensor.homOutTermEquiv line 74
  8. abbrev OAI.ArExplicit.ExternalTensor.homCochainSummand line 79
  9. def OAI.ArExplicit.ExternalTensor.homCochainTermCoordinates line 82
  10. def OAI.ArExplicit.ExternalTensor.homCochainTermEquiv line 91
  11. abbrev OAI.ArExplicit.ExternalTensor.homCochainInclusion line 99
  12. theorem OAI.ArExplicit.ExternalTensor.homCochainTermEquiv_restrict line 104
  13. theorem OAI.ArExplicit.ExternalTensor.homCochainTermCoordinates_inclusion line 116
  14. theorem OAI.ArExplicit.ExternalTensor.homCochainTermEquiv_inclusion_same line 124
  15. theorem OAI.ArExplicit.ExternalTensor.homCochainTermEquiv_inclusion_ne line 131