OAI/Algebra/AuslanderReiten/Algebras/TCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.TIndex line 9
  2. def OAI.ArExplicit.TIndex.number line 13
  3. def OAI.ArExplicit.TIndex.star line 18
  4. def OAI.ArExplicit.T.vector line 28
  5. def OAI.ArExplicit.T.coefficient line 32
  6. theorem OAI.ArExplicit.T.coefficient_lower line 37
  7. theorem OAI.ArExplicit.T.coefficient_upper line 41
  8. theorem OAI.ArExplicit.T.coefficient_lower_upper line 46
  9. theorem OAI.ArExplicit.T.coefficient_upper_lower line 49
  10. theorem OAI.ArExplicit.T.coefficient_vector line 52
  11. theorem OAI.ArExplicit.T.base_expand line 58
  12. theorem OAI.ArExplicit.T.coordinate_ext line 69
  13. theorem OAI.ArExplicit.T.expand line 82
  14. def OAI.ArExplicit.T.coordinateEquiv line 87