OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorBimap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BalancedTensor.bimap line 16

   Source documentation

   The actual balanced tensor map in both variables.

   def bimap (f : M →ₗ[Aᵐᵒᵖ] M') (g : N →ₗ[A] N') : Tensor k A M N →ₗ[k] Tensor k A M' N' :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

2. theorem OAI.LittleFinitistic.BalancedTensor.bimap_mk line 19
3. theorem OAI.LittleFinitistic.BalancedTensor.bimap_comp line 22
4. theorem OAI.LittleFinitistic.BalancedTensor.bimap_zero_left line 29
5. theorem OAI.LittleFinitistic.BalancedTensor.bimap_zero_right line 35