OAI/Algebra/AuslanderReiten/HomComplex/FullHomNaturality.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.mapFullHom_naturalityline 13 - theorem
OAI.ArExplicit.fullHomPostcomp_compline 33 - theorem
OAI.ArExplicit.fullHomPostcomp_precompline 48 - theorem
OAI.ArExplicit.fullHomPrecomp_compline 67