OAI/Algebra/Finitistic/Localization/SignedCochainShift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.signedShiftIso line 11
2. theorem OAI.LittleFinitistic.BimoduleTotal.signedShiftIso_hom_f line 16
3. def OAI.LittleFinitistic.BimoduleTotal.signedShiftComm line 24

   Source documentation

   The standard signed commutation structure for a cochain shift.

   def signedShiftComm (a : ℤ) : (shiftFunctor (CochainComplex C ℤ) a).CommShift ℤ where
   …