OAI/Algebra/AuslanderReiten/Algebras/FrobeniusTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.FrobeniusTrace line 9
2. theorem OAI.ArExplicit.FrobeniusTrace.leftMap_injective line 17
3. def OAI.ArExplicit.FrobeniusTrace.leftEquiv line 27
4. theorem OAI.ArExplicit.FrobeniusTrace.leftEquiv_apply line 34
5. def OAI.ArExplicit.FrobeniusTrace.dualEquiv line 37
6. theorem OAI.ArExplicit.FrobeniusTrace.dualEquiv_apply line 40
7. theorem OAI.ArExplicit.FrobeniusTrace.regular_injective line 44
8. def OAI.ArExplicit.trivialExtensionFrobeniusTrace line 50