OAI/Algebra/AuslanderReiten/Stable/TensorStableEnd.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.A.simple_not_projective line 13
  2. theorem OAI.ArExplicit.A.simple_scalar_generator line 20
  3. def OAI.ArExplicit.A.endScalar line 26
  4. theorem OAI.ArExplicit.A.end_eq_scalar_id line 34
  5. def OAI.ArExplicit.A.simpleEndEquiv line 48
  6. theorem OAI.ArExplicit.A.stable_identity_ne_zero line 58
  7. theorem OAI.ArExplicit.A.simpleEnd_classOf_injective line 66
  8. def OAI.ArExplicit.A.stableEndEquiv line 78
  9. theorem OAI.ArExplicit.A.stableEndEquiv_classOf line 84
  10. theorem OAI.ArExplicit.A.stableEndEquiv_identity line 92