OAI/Algebra/AuslanderReiten/Bar/NativeBarFreeEndpoint.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.ModuleBar.canonicalCoefficientTensor line 15
  2. theorem OAI.ArExplicit.ModuleBar.coefficientScalarIso_tmul line 18
  3. def OAI.ArExplicit.BarBalanced.canonicalEvaluatedTensor line 33
  4. def OAI.ArExplicit.BarBalanced.nativeFreeEndpoint line 37
  5. theorem OAI.ArExplicit.BarBalanced.canonicalComplexIso_tensor line 43
  6. theorem OAI.ArExplicit.BarBalanced.nativeComplexIso_component line 47
  7. theorem OAI.ArExplicit.BarBalanced.nativeFreeEndpoint_component line 52
  8. theorem OAI.ArExplicit.BarBalanced.compValues line 59
  9. theorem OAI.ArExplicit.BarBalanced.nativeScalarValues line 64
  10. theorem OAI.ArExplicit.BarBalanced.nativeFreeValues line 74
  11. theorem OAI.ArExplicit.BarBalanced.valueOfEq line 88
  12. theorem OAI.ArExplicit.BarBalanced.nativeFreeEndpoint_tensor line 92