OAI/CategoryTheory/ThickClosure/CyclicShift.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HahnWilson.CyclicShift.cyclicShift line 16
2. def OAI.HahnWilson.CyclicShift.shiftZeroIso line 39
3. def OAI.HahnWilson.CyclicShift.shiftAddIso line 45
4. theorem OAI.HahnWilson.CyclicShift.shift_zero line 62
5. theorem OAI.HahnWilson.CyclicShift.shift_add line 64
6. def OAI.HahnWilson.CyclicShift.unrollShiftIso line 68
7. theorem OAI.HahnWilson.CyclicShift.unroll_shift line 85
8. instance OAI.HahnWilson.CyclicShift.(instance at line 93) line 93
9. lemma OAI.HahnWilson.CyclicShift.shiftZero_hom_f line 119
10. lemma OAI.HahnWilson.CyclicShift.shiftAdd_hom_f line 123
11. instance OAI.HahnWilson.CyclicShift.(instance at line 128) line 128
12. lemma OAI.HahnWilson.CyclicShift.quasiIso_iff_unroll line 168
13. lemma OAI.HahnWilson.CyclicShift.quasiIso_shift_iff line 184
14. instance OAI.HahnWilson.CyclicShift.quasiIso_isCompatibleWithShift line 196