Theorem RatFunc.WithZero.valued_def

Modification history

2025-08-13 15:11
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
chore: fix namespace of RatFunc.WithZero.valued_def (#27997) …
Deleted RatFunc.WithZero.valued_defView on Github →
2024-07-05 11:29
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
feat: add properties of the X-adic valuation on `PowerSeries K` (#13064) …
Added RatFunc.WithZero.valued_defView on Github →