Theorem LaurentSeries.LaurentSeries_coe

Modification history

2026-03-05 14:15
Mathlib/RingTheory/LaurentSeries.lean
feat(RatFunc): add notation for RatFunc (#36172) …
Modified LaurentSeries.LaurentSeries_coeView on Github →
2026-03-02 10:51
Mathlib/RingTheory/LaurentSeries.lean
refactor: use 1-field structure to define the `WithVal` type synonym (#34049) …
Modified LaurentSeries.LaurentSeries_coeView on Github →
2024-11-09 09:51
Mathlib/RingTheory/LaurentSeries.lean
feat(RingTheory/LaurentSeries): finishes the proof that LaurentSeries are the X-adic completion of Rational Functions (#18346) …
Added LaurentSeries.LaurentSeries_coeView on Github →