OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleTotalCongruence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleComplexTensor.rightTotalEquiv line 15
2. theorem OAI.LittleFinitistic.BimoduleComplexTensor.right_entry line 18
3. theorem OAI.LittleFinitistic.BimoduleComplexTensor.right_differential line 28
4. def OAI.LittleFinitistic.BimoduleComplexTensor.totalRightIso line 50

   Source documentation

   Tensor total preserves actual isomorphisms of genuine bimodule complexes and their outside action.

   def totalRightIso : total k S A Q Z p hp ≅ total k S A Q' Z p hp :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.total