OAI/Algebra/AuslanderReiten/Cocycles/CocycleRelative.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.CocycleData.vertexSpaceline 11 - theorem
OAI.ArExplicit.CocycleData.vertexSpace_inductionline 14 - theorem
OAI.ArExplicit.CocycleData.p_normalized_first_relativeline 28 - theorem
OAI.ArExplicit.CocycleData.p_normalized_second_relativeline 37 - theorem
OAI.ArExplicit.CocycleData.p_normalized_third_relativeline 46 - theorem
OAI.ArExplicit.CocycleData.p_balanced_first_relativeline 55 - theorem
OAI.ArExplicit.CocycleData.p_balanced_second_relativeline 64 - theorem
OAI.ArExplicit.CocycleData.p_left_relativeline 73 - theorem
OAI.ArExplicit.CocycleData.p_right_relativeline 82