Theorem LaurentSeries.exists_ratFunc_eq_v

Modification history

2025-09-26 20:32
Mathlib/RingTheory/LaurentSeries.lean
chore(RingTheory/Laurent): use WithZero.exp to golf statements and proofs about valuation on K((X)) (#27339) …
Added LaurentSeries.exists_ratFunc_eq_vView on Github →