Commit 2025-09-26 20:32 1fb1d7f4
View on Github →chore(RingTheory/Laurent): use WithZero.exp to golf statements and proofs about valuation on K((X)) (#27339)
Done as part of refactor of Valued in #27314. This PR does not change any definitions. Instead, uses WithZero.exp instead of coercion + Multiplicative.ofAdd. And some helper simp lemmas about valuations of RatFunc vis a vis LaurentSeries.