OAI/Algebra/FinitisticAsymmetry/Nakayama/Modules.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.Nakayama.rightMult line 13
  2. lemma OAI.LittleFinitistic.Nakayama.rightMult_apply line 16
  3. def OAI.LittleFinitistic.Nakayama.Object line 19
  4. def OAI.LittleFinitistic.Nakayama.Object.value line 23
  5. instance OAI.LittleFinitistic.Nakayama.Object.(instance at line 24) line 24
  6. instance OAI.LittleFinitistic.Nakayama.Object.(instance at line 25) line 25
  7. lemma OAI.LittleFinitistic.Nakayama.Object.ext line 26
  8. instance OAI.LittleFinitistic.Nakayama.Object.(instance at line 27) line 27
  9. instance OAI.LittleFinitistic.Nakayama.Object.(instance at line 58) line 58
  10. instance OAI.LittleFinitistic.Nakayama.Object.(instance at line 60) line 60
  11. def OAI.LittleFinitistic.Nakayama.map line 71
  12. def OAI.LittleFinitistic.Nakayama.functor line 81
  13. instance OAI.LittleFinitistic.Nakayama.(instance at line 86) line 86
  14. abbrev OAI.LittleFinitistic.Nakayama.coind line 102
  15. instance OAI.LittleFinitistic.Nakayama.coind_modulek line 105
  16. instance OAI.LittleFinitistic.Nakayama.coind_tower line 109
  17. instance OAI.LittleFinitistic.Nakayama.coind_comm line 120
  18. lemma OAI.LittleFinitistic.Nakayama.field_injective line 123
  19. instance OAI.LittleFinitistic.Nakayama.coind_injective line 132
  20. abbrev OAI.LittleFinitistic.Nakayama.DA line 136
  21. def OAI.LittleFinitistic.Nakayama.daEquiv line 138
  22. def OAI.LittleFinitistic.Nakayama.etaMap line 158
  23. lemma OAI.LittleFinitistic.Nakayama.etaMap_apply line 167
  24. lemma OAI.LittleFinitistic.Nakayama.eta_natural line 170
  25. structure OAI.LittleFinitistic.Nakayama.Frame line 173
  26. lemma OAI.LittleFinitistic.Nakayama.frame_nonempty line 179
  27. lemma OAI.LittleFinitistic.Nakayama.Frame.dual_expand line 193
  28. lemma OAI.LittleFinitistic.Nakayama.eta_injective line 201
  29. lemma OAI.LittleFinitistic.Nakayama.eta_surjective line 213
  30. lemma OAI.LittleFinitistic.Nakayama.coind_smul_eval line 247
  31. lemma OAI.LittleFinitistic.Nakayama.coind_add_eval line 252
  32. def OAI.LittleFinitistic.Nakayama.coindInclusion line 255
  33. def OAI.LittleFinitistic.Nakayama.coindRetraction line 274
  34. lemma OAI.LittleFinitistic.Nakayama.coindInclusion_retraction line 305
  35. lemma OAI.LittleFinitistic.Nakayama.object_injective line 315