OAI/Algebra/AuslanderReiten/Coordinates/TensorNormalizedTop.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.T.sourceUnit line 24
  2. theorem OAI.ArExplicit.T.sourceAugmentationEquiv_unit line 26
  3. theorem OAI.ArExplicit.T.finiteSourceTop_unit line 33
  4. def OAI.ArExplicit.T.normalizedSourceTop line 45
  5. theorem OAI.ArExplicit.T.normalizedLift_top line 49
  6. def OAI.ArExplicit.T.endpointEvaluation line 71
  7. theorem OAI.ArExplicit.T.endpointEvaluation_unit line 78
  8. theorem OAI.ArExplicit.T.normalizedSourceTop_evaluated line 86