OAI/Algebra/Finitistic/Tensor/BalancedTensorMaps.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Tensor an actual right-module homomorphism with the identity.

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

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor

2. theorem OAI.LittleFinitistic.BalancedTensor.mapLeft_mk line 23
3. theorem OAI.LittleFinitistic.BalancedTensor.mapLeft_id line 26
4. theorem OAI.LittleFinitistic.BalancedTensor.mapLeft_comp line 31
5. theorem OAI.LittleFinitistic.BalancedTensor.mapLeft_add line 37