OAI/Algebra/Finitistic/Bimodule/BimoduleTensorAcross.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.tensorAcross line 14

   Source documentation

   Tensor a bimodule map and an input map, retaining the outside B-action.

   def tensorAcross (f : M ⟶ M') (g : N ⟶ N') :
       InputTensor k B M N →ₗ[B] InputTensor k B M' N' :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.InputTensor

2. theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_mk line 19
3. theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_comp line 25
4. theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_id line 37
5. theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_zero_left line 48
6. theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_zero_right line 61
7. theorem OAI.LittleFinitistic.BimoduleTotal.tensorAcross_eq_termMap line 77