Theorem Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X

Modification history

2026-03-18 07:57
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) (#30505) …
Modified Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_XView on Github →
2025-07-09 13:45
Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
feat: valuation on RatFunc which is trivial on constants (#24254) …
Added Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_XView on Github →