OAI/Algebra/Finitistic/Ordinary/OrdinaryLeftTensorMaps.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.LeftTensor.bimap line 17

   Source documentation

   The actual balanced bimap retains the outside left action.

   def bimap (f : M →ₗ[Aᵐᵒᵖ] M') (hf : ∀ (s : S) m, f (s • m) = s • f m)
       (g : N →ₗ[A] N') : LeftTensor k A S M N →ₗ[S] LeftTensor k A S M' N' where
   …

   Mentions: OAI.LittleFinitistic.LeftTensor

2. theorem OAI.LittleFinitistic.LeftTensor.bimap_mk line 36