OAI/CategoryTheory/ThickClosure/Coefficients.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HahnWilson.LaurentDg.coefficientModule line 14
  2. def OAI.HahnWilson.LaurentDg.coefficientConst line 16
  3. def OAI.HahnWilson.LaurentDg.coefficientEval line 18
  4. def OAI.HahnWilson.LaurentDg.coefficientToPiece line 21
  5. def OAI.HahnWilson.LaurentDg.coefficientTo line 27
  6. lemma OAI.HahnWilson.LaurentDg.coefficientTo_inc line 30
  7. def OAI.HahnWilson.LaurentDg.coefficientFrom line 34
  8. lemma OAI.HahnWilson.LaurentDg.coefficientFrom_single line 38
  9. lemma OAI.HahnWilson.LaurentDg.coefficientTo_monomial line 49
  10. lemma OAI.HahnWilson.LaurentDg.coefficientTo_from line 59
  11. lemma OAI.HahnWilson.LaurentDg.coefficientFrom_to line 66
  12. def OAI.HahnWilson.LaurentDg.coefficientEquiv line 94
  13. lemma OAI.HahnWilson.LaurentDg.coefficient_power_const line 100
  14. lemma OAI.HahnWilson.LaurentDg.coefficient_act_const line 109
  15. lemma OAI.HahnWilson.LaurentDg.coefficient_act_from line 120
  16. lemma OAI.HahnWilson.LaurentDg.coefficient_differential_zero line 136
  17. theorem OAI.HahnWilson.LaurentDg.coefficient_regular_aux line 148
  18. theorem OAI.HahnWilson.LaurentDg.coefficient_regular line 163