Theorem LaurentSeries.valuation_coe_ratFunc

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.valuation_coe_ratFuncView on Github →