OAI/RingTheory/Kurosh/FreeSeries.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Noncommutative formal series and their ring operations.

  1. structure OAI.KuroshConstruction.FreeSeries line 9
  2. theorem OAI.KuroshConstruction.FreeSeries.coeff_injective line 16
  3. instance OAI.KuroshConstruction.FreeSeries.(instance at line 19) line 19
  4. instance OAI.KuroshConstruction.FreeSeries.(instance at line 21) line 21
  5. instance OAI.KuroshConstruction.FreeSeries.(instance at line 23) line 23
  6. instance OAI.KuroshConstruction.FreeSeries.(instance at line 25) line 25
  7. instance OAI.KuroshConstruction.FreeSeries.(instance at line 27) line 27
  8. instance OAI.KuroshConstruction.FreeSeries.(instance at line 29) line 29
  9. theorem OAI.KuroshConstruction.FreeSeries.coeff_zero line 31
  10. theorem OAI.KuroshConstruction.FreeSeries.coeff_add line 33
  11. theorem OAI.KuroshConstruction.FreeSeries.coeff_neg line 36
  12. theorem OAI.KuroshConstruction.FreeSeries.coeff_sub line 39
  13. instance OAI.KuroshConstruction.FreeSeries.(instance at line 42) line 42
  14. def OAI.KuroshConstruction.FreeSeries.productCoeff line 46
  15. instance OAI.KuroshConstruction.FreeSeries.(instance at line 50) line 50
  16. theorem OAI.KuroshConstruction.FreeSeries.coeff_mul_nil line 53
  17. theorem OAI.KuroshConstruction.FreeSeries.coeff_mul_cons line 56
  18. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_zero_left line 64
  19. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_zero_right line 72
  20. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_add_left line 78
  21. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_add_right line 88
  22. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_mul_left line 96
  23. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_assoc line 102
  24. def OAI.KuroshConstruction.FreeSeries.const line 114
  25. instance OAI.KuroshConstruction.FreeSeries.(instance at line 116) line 116
  26. instance OAI.KuroshConstruction.FreeSeries.(instance at line 118) line 118
  27. instance OAI.KuroshConstruction.FreeSeries.(instance at line 120) line 120
  28. lemma OAI.KuroshConstruction.FreeSeries.coeff_const_nil line 122
  29. lemma OAI.KuroshConstruction.FreeSeries.coeff_const_cons line 124
  30. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_const_left line 127
  31. lemma OAI.KuroshConstruction.FreeSeries.productCoeff_const_right line 136
  32. instance OAI.KuroshConstruction.FreeSeries.(instance at line 142) line 142