Theorem PowerSeries.intValuation_X

Modification history

2025-05-17 21:17

Mathlib/RingTheory/LaurentSeries.lean

chore(RingTheory/DedekindDomain/AdicValuation): Use intValuation over intValuationDef (#24644) …

Modified PowerSeries.intValuation_X View 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_X View on Github →