OAI/Algebra/Finitistic/Rectification/FullTensorProperties.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.FullTensorProperties.inputEquiv line 16

   Source documentation

   The tensor input's scalar structure agrees with the original bimodule's scalar restriction through the two algebra homomorphisms.

   def inputEquiv (M : ModuleCat.{u} (Enveloping k B)) :
       (forgetK k B).obj M ≃ₗ[k] BimoduleBalancedTensor.Input k B M where
   …

   Mentions: OAI.LittleFinitistic.BimoduleBalancedTensor.Input

2. theorem OAI.LittleFinitistic.FullTensorProperties.finite line 32
3. theorem OAI.LittleFinitistic.FullTensorProperties.bounded line 43