Commit 2024-10-22 09:16 1460f4a0

View on Github →

feat(RingTheory/LaurentSeries): composition of Hasse Derivatives (#16106) This PR proves basic properties of Hasse derivatives of Laurent series including composition, and introduces the derivative as a linear map.

Estimated changes

Modified Mathlib/RingTheory/HahnSeries/Addition.lean

added theorem HahnSeries.nsmul_coeff

Modified Mathlib/RingTheory/LaurentSeries.lean

added def LaurentSeries.derivative

added theorem LaurentSeries.derivative_apply

added theorem LaurentSeries.derivative_iterate

added theorem LaurentSeries.derivative_iterate_coeff

modified theorem LaurentSeries.hasseDeriv_coeff

added theorem LaurentSeries.hasseDeriv_comp

added theorem LaurentSeries.hasseDeriv_comp_coeff

added theorem LaurentSeries.hasseDeriv_single

added theorem LaurentSeries.hasseDeriv_single_add

added theorem LaurentSeries.hasseDeriv_zero