OAI/Algebra/AuslanderReiten/Homology/LinearHomologyCongr.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.LinearHomology.cycleEquivline 19 - theorem
OAI.ArExplicit.LinearHomology.cycleEquiv_boundariesline 32 - def
OAI.ArExplicit.LinearHomology.congrline 44 - theorem
OAI.ArExplicit.LinearHomology.congr_mkline 49 - theorem
OAI.ArExplicit.LinearHomology.congr_symm_mkline 54