OAI/Algebra/AuslanderReiten/Fibers/ExplicitBimoduleFiber.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.T.fiberTarget line 14
  2. def OAI.ArExplicit.T.normalizedLift line 16
  3. theorem OAI.ArExplicit.T.normalizedLift_apply line 20
  4. abbrev OAI.ArExplicit.T.finiteFiber line 23
  5. abbrev OAI.ArExplicit.T.explicitBimodule line 27
  6. def OAI.ArExplicit.T.rho₁ line 31
  7. def OAI.ArExplicit.T.rho₂ line 36
  8. def OAI.ArExplicit.T.explicitFiberSequence line 41
  9. theorem OAI.ArExplicit.T.explicitFiberSequence_shortExact line 46
  10. theorem OAI.ArExplicit.T.explicitBimodule_finite_k line 51
  11. theorem OAI.ArExplicit.T.explicitBimodule_left line 54
  12. theorem OAI.ArExplicit.T.explicitBimodule_right line 62