OAI/Algebra/AuslanderReiten/Algebras/TSimple.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.TrivialExtension.baseProjectionline 13 - def
OAI.ArExplicit.T.simpleCharacterline 27 - instance
OAI.ArExplicit.Resolution.(instance at line 42)line 42 - theorem
OAI.ArExplicit.Resolution.t_smul_simpleline 45 - instance
OAI.ArExplicit.Resolution.(instance at line 48)line 48 - theorem
OAI.ArExplicit.Resolution.t_simple_characterline 53 - theorem
OAI.ArExplicit.Resolution.dual_ideal_annihilates_simpleline 57