OAI/Algebra/AuslanderReiten/Fibers/ConcreteFiberProfile.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.T.normalizedBranches_equal line 22
2. theorem OAI.ArExplicit.T.normalizedBranch_ne_zero line 25
3. theorem OAI.ArExplicit.T.fiberPositiveRhoPair_bijective line 28
4. def OAI.ArExplicit.T.fiberDiagonalClass line 35
5. theorem OAI.ArExplicit.T.fiberDiagonalClass_image line 41
6. theorem OAI.ArExplicit.T.fiberDiagonalClass_spans line 49
7. theorem OAI.ArExplicit.T.fiberDiagonalClass_ne_zero line 56