OAI/Algebra/AuslanderReiten/Fibers/ConcreteFiberHomCoordinates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

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

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

2. abbrev OAI.ArExplicit.T.SimpleHom line 20
3. abbrev OAI.ArExplicit.T.FiberHom line 21
4. abbrev OAI.ArExplicit.T.MiddleHom line 22
5. def OAI.ArExplicit.T.middleHomEquiv line 24
6. def OAI.ArExplicit.T.fiberHomInclusion line 30
7. def OAI.ArExplicit.T.fiberHomRhoPair line 35
8. theorem OAI.ArExplicit.T.middleHomEquiv_inclusion line 44