OAI/Algebra/AuslanderReiten/Coordinates/ConcreteCubicAction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.T.simpleHomotopyObject line 20

   Distinct definitions of this name: OAI/Algebra/AuslanderReiten/Fibers/ConcreteFiberHomCoordinates.lean:17 (different declaration text). Qualify references as OAI.ArExplicit.T.simpleHomotopyObject@path.

2. theorem OAI.ArExplicit.T.evaluatedFirstCokernel_fullHom_action line 24
3. theorem OAI.ArExplicit.T.evaluatedSecondCokernel_fullHom_action line 38