Theorem LaurentSeries.comparePkg_eq_extension

Modification history

2026-03-02 10:51
Mathlib/RingTheory/LaurentSeries.lean
refactor: use 1-field structure to define the `WithVal` type synonym (#34049) …
Modified LaurentSeries.comparePkg_eq_extensionView 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.comparePkg_eq_extensionView on Github →