OAI/RingTheory/Kurosh/SeriesAlgebra.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Constant coefficients, scalar maps, and linear coefficients of formal series.

  1. lemma OAI.KuroshConstruction.FreeSeries.coeff_one line 12
  2. lemma OAI.KuroshConstruction.FreeSeries.coeff_const line 15
  3. lemma OAI.KuroshConstruction.FreeSeries.const_mul_coeff line 18
  4. lemma OAI.KuroshConstruction.FreeSeries.mul_const_coeff line 21
  5. def OAI.KuroshConstruction.FreeSeries.constHom line 24
  6. def OAI.KuroshConstruction.FreeSeries.constantCoeff line 31
  7. lemma OAI.KuroshConstruction.FreeSeries.constantCoeff_const line 38
  8. instance OAI.KuroshConstruction.FreeSeries.(instance at line 40) line 40
  9. lemma OAI.KuroshConstruction.FreeSeries.coeff_algebraMap line 46
  10. lemma OAI.KuroshConstruction.FreeSeries.coeff_smul line 49
  11. def OAI.KuroshConstruction.FreeSeries.constantCoeffAlgHom line 54
  12. def OAI.KuroshConstruction.FreeSeries.constAlgHom line 57
  13. def OAI.KuroshConstruction.FreeSeries.map line 60
  14. def OAI.KuroshConstruction.FreeSeries.letterCoeff line 77
  15. def OAI.KuroshConstruction.FreeSeries.letter line 79
  16. lemma OAI.KuroshConstruction.FreeSeries.coeff_letter line 81
  17. lemma OAI.KuroshConstruction.FreeSeries.constantCoeff_letter line 84
  18. lemma OAI.KuroshConstruction.FreeSeries.letterCoeff_letter line 87
  19. lemma OAI.KuroshConstruction.FreeSeries.letter_commutes_const line 91
  20. lemma OAI.KuroshConstruction.FreeSeries.letterCoeff_mul line 97