OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleTotalAssociativity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleComplexTensor.associativeTotalEquiv line 19
2. theorem OAI.LittleFinitistic.BimoduleComplexTensor.associative_entry line 24
3. theorem OAI.LittleFinitistic.BimoduleComplexTensor.associative_vertical line 44
4. theorem OAI.LittleFinitistic.BimoduleComplexTensor.associative_differential line 56
5. def OAI.LittleFinitistic.BimoduleComplexTensor.totalAssociativityIso line 83

   Source documentation

   Full signed total associativity in S-modules, on every input complex Z.

   def totalAssociativityIso :
       total k S B (middleBimoduleComplex k S A B N Q) Z p hp ≅
         total k S A Q (middleLeftComplex k A B N Z) p hp :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.total, OAI.LittleFinitistic.BimoduleComplexTensor.middleBimoduleComplex, OAI.LittleFinitistic.middleLeftComplex