Theorem LaurentSeries.valuation_def

Modification history

2025-07-04 09:20

Mathlib/RingTheory/LaurentSeries.lean

feat(WithZero): `exp : ℤ → ℤᵐ⁰`, `log : ℤᵐ⁰ → ℤ` (#24977) …

Modified LaurentSeries.valuation_def View on Github →

2025-03-26 19:05

Mathlib/RingTheory/LaurentSeries.lean

chore(RingTheory): `erw` cleanup from A to LocalRing (#23343) …

Added LaurentSeries.valuation_def View on Github →