OAI/Algebra/AuslanderReiten/Homology/LinearCokernelMap.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.LinearCokernel.mapline 13 - theorem
OAI.ArExplicit.LinearCokernel.map_mkline 21 - theorem
OAI.ArExplicit.LinearCokernel.inverse_squareline 25 - def
OAI.ArExplicit.LinearCokernel.equivline 33 - theorem
OAI.ArExplicit.LinearCokernel.equiv_mkline 47