OAI/Algebra/AuslanderReiten/Evaluation/TensorBetaEvaluation.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.A.barZeroCoordinateline 12 - theorem
OAI.ArExplicit.A.barZeroCoordinate_tmulline 16 - theorem
OAI.ArExplicit.A.squareEvaluation_eq_betaline 21 - theorem
OAI.ArExplicit.A.squareEvaluation_coordinate_ne_zeroline 30