OAI/Algebra/AuslanderReiten/Evaluation/ConcreteBranchDetector.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.T.branchBetaDetector_eq_betaline 14 - theorem
OAI.ArExplicit.T.branchHom_common_of_scalarCoordinateline 27 - theorem
OAI.ArExplicit.T.branchHom_ne_zero_of_scalarCoordinateline 33