Theorem PowerSeries.intValuation_X

Modification history

2025-10-22 23:09
Mathlib/RingTheory/LaurentSeries.lean
chore(RingTheory/AdicValuation,LaurentSeries): switch to `WithZero.exp` instead of coercions of `Multiplicative.ofAdd` (#29642) …
Modified PowerSeries.intValuation_XView on Github →
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) …
Modified PowerSeries.intValuation_XView on Github →
2025-05-17 21:17
Mathlib/RingTheory/LaurentSeries.lean
chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef (#24644) …
Modified PowerSeries.intValuation_XView on Github →
2024-07-05 11:29
Mathlib/RingTheory/LaurentSeries.lean
feat: add properties of the X-adic valuation on `PowerSeries K` (#13064) …
Added PowerSeries.intValuation_XView on Github →