OAI/Algebra/Finitistic/Bimodule/BimoduleShiftTotal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.BimoduleTotal.shiftTermIso line 13
2. theorem OAI.LittleFinitistic.BimoduleTotal.shiftTerm_hom_apply line 18
3. def OAI.LittleFinitistic.BimoduleTotal.shiftTotalIso line 24

   Source documentation

   The complete signed total commutes with every integer shift, with the actual horizontal maps.

   def shiftTotalIso (s : ℤ) : total k B P p hp (Z⟦s⟧) ≅ (total k B P p hp Z)⟦s⟧ :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleTotal.total