OAI/Algebra/AuslanderReiten/Algebras/TensorFrobenius.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.FrobeniusTrace.tensorTrace line 16
2. theorem OAI.ArExplicit.FrobeniusTrace.tensorTrace_tmul line 20
3. def OAI.ArExplicit.FrobeniusTrace.tensorDualEquiv line 23
4. theorem OAI.ArExplicit.FrobeniusTrace.tensorDualEquiv_apply line 27
5. def OAI.ArExplicit.FrobeniusTrace.tensor line 37
6. theorem OAI.ArExplicit.FrobeniusTrace.tensorTrace_mul_comm line 47
7. def OAI.ArExplicit.AFrobeniusTrace line 62
8. instance OAI.ArExplicit.(instance at line 66) line 66
9. theorem OAI.ArExplicit.A_trace_symmetric line 69