OAI/Algebra/AuslanderReiten/Tensor/ExternalBalancedNaturality.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.ExternalBalanced.balancedMapline 15 - theorem
OAI.ArExplicit.ExternalBalanced.balancedMap_tmulline 23 - def
OAI.ArExplicit.ExternalBalanced.exteriorMapline 33 - theorem
OAI.ArExplicit.ExternalBalanced.coordinates_mapline 41 - theorem
OAI.ArExplicit.ExternalBalanced.scalarCoordinates_mapline 49 - theorem
OAI.ArExplicit.ExternalBalanced.shuffle_naturalline 55