Theorem LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero

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_le_iff_coeff_lt_log_eq_zeroView on Github →