OAI/Algebra/AuslanderReiten/Ext/ExtKunnethActions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.ExternalTensor.firstActionUnderKunneth line 22
  2. theorem OAI.ArExplicit.ExternalTensor.firstActionUnderKunneth_elementary line 30
  3. theorem OAI.ArExplicit.ExternalTensor.coefficients_ext line 49
  4. theorem OAI.ArExplicit.ExternalTensor.firstActionUnderKunneth_eq line 72
  5. theorem OAI.ArExplicit.ExternalTensor.firstCubicExt_kunneth line 81
  6. theorem OAI.ArExplicit.ExternalTensor.firstCubicExt_kunneth_of_class line 94
  7. def OAI.ArExplicit.ExternalTensor.secondActionUnderKunneth line 105
  8. theorem OAI.ArExplicit.ExternalTensor.secondActionUnderKunneth_elementary line 113
  9. theorem OAI.ArExplicit.ExternalTensor.secondActionUnderKunneth_eq line 130
  10. theorem OAI.ArExplicit.ExternalTensor.secondCubicExt_kunneth line 139
  11. theorem OAI.ArExplicit.ExternalTensor.secondCubicExt_kunneth_of_class line 152