OAI/Algebra/Finitistic/Bimodule/BimoduleBalancedTensor.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleBalancedTensor.Input line 16
2. abbrev OAI.LittleFinitistic.BimoduleBalancedTensor.Tensor line 20
3. def OAI.LittleFinitistic.BimoduleBalancedTensor.inputAction line 22
4. def OAI.LittleFinitistic.BimoduleBalancedTensor.action line 27

   Source documentation

   The original left B action on a genuine bimodule descends through balancing over B.

   def action : B →+* Module.End k (Tensor k B M N) where
   …

   Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.Tensor

5. instance OAI.LittleFinitistic.BimoduleBalancedTensor.leftModule line 59
6. theorem OAI.LittleFinitistic.BimoduleBalancedTensor.smul_mk line 62