OAI/Algebra/AuslanderReiten/Tensor/ExternalBalancedCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.ExternalBalanced.exteriorBimodule line 18
2. def OAI.ArExplicit.ExternalBalanced.bimoduleCoordinates line 22
3. theorem OAI.ArExplicit.ExternalBalanced.bimoduleCoordinates_symm_tmul line 30
4. theorem OAI.ArExplicit.ExternalBalanced.bimoduleCoordinates_right line 35
5. theorem OAI.ArExplicit.ExternalBalanced.bimoduleCoordinates_left line 47