OAI/Algebra/Finitistic/Selected/SelectedNativeEvaluation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedNativeEvaluation.H line 14
2. instance OAI.LittleFinitistic.SelectedNativeEvaluation.(instance at line 15) line 15
3. def OAI.LittleFinitistic.SelectedNativeEvaluation.HK line 19
4. def OAI.LittleFinitistic.SelectedNativeEvaluation.HDerived line 20
5. def OAI.LittleFinitistic.SelectedNativeEvaluation.imageIsoK line 22
6. def OAI.LittleFinitistic.SelectedNativeEvaluation.imageIso line 25
7. abbrev OAI.LittleFinitistic.SelectedNativeEvaluation.target line 29

   Source documentation

   The actual primary H(Y), concentrated in degree zero, and its shift by three.

   abbrev target := HDerived (Y := Y) ⊞ (HDerived (Y := Y))⟦(3 : ℤ)⟧

   Mentions: OAI.LittleFinitistic.SelectedNativeEvaluation.HDerived

8. def OAI.LittleFinitistic.SelectedNativeEvaluation.targetIso line 30
9. def OAI.LittleFinitistic.SelectedNativeEvaluation.V0Iso line 34
10. def OAI.LittleFinitistic.SelectedNativeEvaluation.D0Iso line 37
11. def OAI.LittleFinitistic.SelectedNativeEvaluation.D1Iso line 39
12. def OAI.LittleFinitistic.SelectedNativeEvaluation.D2Iso line 41