OAI/Algebra/AuslanderReiten/Basic.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.GorensteinProjectiveline 21 - def
OAI.ArExplicit.PositiveExtVanishline 33 - def
OAI.ArExplicit.MainConclusionsline 39 - structure
OAI.ArExplicit.Candidateline 52 - def
OAI.ArExplicit.FullMainTheoremline 65