OAI/Algebra/AuslanderReiten/Tensor/EnvelopingStableEvaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.EnvelopingBimodule.tensorMap_smul_linear line 21
2. def OAI.ArExplicit.EnvelopingBimodule.tensorHom line 35
3. theorem OAI.ArExplicit.EnvelopingBimodule.tensorHom_projective line 44
4. def OAI.ArExplicit.EnvelopingBimodule.stableEvaluation line 62
5. theorem OAI.ArExplicit.EnvelopingBimodule.stableEvaluation_classOf line 71
6. def OAI.ArExplicit.EnvelopingBimodule.stableEvaluationLinear line 76
7. theorem OAI.ArExplicit.EnvelopingBimodule.stableEvaluation_id line 88
8. theorem OAI.ArExplicit.EnvelopingBimodule.stableEvaluation_comp line 94