OAI/Algebra/Finitistic/Localization/TensorEvaluationFunctor.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BalancedTensor.ScalarModule line 11
2. instance OAI.LittleFinitistic.BalancedTensor.scalarModuleTower line 14
3. def OAI.LittleFinitistic.BalancedTensor.tensorFunctor line 23

   Source documentation

   The actual tensor evaluation functor on all right A-modules.

   def tensorFunctor : ModuleCat.{w} Aᵐᵒᵖ ⥤ ModuleCat.{max w z} k where
   …

4. instance OAI.LittleFinitistic.BalancedTensor.tensorFunctorAdditive line 34