OAI/CategoryTheory/ThickClosure/PerfectModules.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HahnWilson.LaurentDg.total line 15
  2. abbrev OAI.HahnWilson.LaurentDg.inc line 16
  3. lemma OAI.HahnWilson.LaurentDg.power_cast line 19
  4. def OAI.HahnWilson.LaurentDg.move line 21
  5. lemma OAI.HahnWilson.LaurentDg.move_congr line 24
  6. def OAI.HahnWilson.LaurentDg.shiftPower line 30
  7. lemma OAI.HahnWilson.LaurentDg.shiftPower_inc line 33
  8. lemma OAI.HahnWilson.LaurentDg.shiftPower_move line 37
  9. lemma OAI.HahnWilson.LaurentDg.move_self line 46
  10. lemma OAI.HahnWilson.LaurentDg.shiftPower_zero line 49
  11. lemma OAI.HahnWilson.LaurentDg.shiftPower_add line 55
  12. def OAI.HahnWilson.LaurentDg.powerRepresentation line 64
  13. def OAI.HahnWilson.LaurentDg.laurentRepresentation line 72
  14. lemma OAI.HahnWilson.LaurentDg.laurentRepresentation_single line 80
  15. def OAI.HahnWilson.LaurentDg.totalDifferential line 88
  16. lemma OAI.HahnWilson.LaurentDg.totalDifferential_inc line 92
  17. lemma OAI.HahnWilson.LaurentDg.totalDifferential_inc_succ line 97
  18. lemma OAI.HahnWilson.LaurentDg.totalDifferential_sq line 105
  19. lemma OAI.HahnWilson.LaurentDg.totalDifferential_shiftPower line 116
  20. lemma OAI.HahnWilson.LaurentDg.laurentRepresentation_commute line 132
  21. theorem OAI.HahnWilson.LaurentDg.actual_laurent_action line 146