OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleAssociativity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleAssociativity.coefficient line 22
2. abbrev OAI.LittleFinitistic.BimoduleAssociativity.source line 24
3. abbrev OAI.LittleFinitistic.BimoduleAssociativity.target line 25
4. def OAI.LittleFinitistic.BimoduleAssociativity.scalarEquiv line 27
5. theorem OAI.LittleFinitistic.BimoduleAssociativity.scalarEquiv_mk line 33
6. theorem OAI.LittleFinitistic.BimoduleAssociativity.coefficient_smul_mk line 38
7. theorem OAI.LittleFinitistic.BimoduleAssociativity.scalarEquiv_smul_mk line 44
8. def OAI.LittleFinitistic.BimoduleAssociativity.equivalence line 58

   Source documentation

   Ordinary balanced associativity retains the actual outside left action.

   def equivalence : source k S A B M N Z ≃ₗ[S] target k S A B M N Z where
   …

   Mentions: OAI.LittleFinitistic.BimoduleAssociativity.source, OAI.LittleFinitistic.BimoduleAssociativity.target