Commit 2026-03-18 07:57 2749d583

View on Github →

feat(NumberTheory/RatFunc/Ostrowski): prove Ostrowski's theorem for K(X) (#30505) We prove Ostrowski's theorem for the field of rational functions K(X), where K is any field.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

modified theorem Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X

added theorem RatFunc.coePolynomial_eq_algebraMap

Modified Mathlib/FieldTheory/RatFunc/Degree.lean

added theorem RatFunc.intDegree_div

Modified Mathlib/NumberTheory/FunctionField.lean

Created Mathlib/NumberTheory/RatFunc/Ostrowski.lean

added theorem RatFunc.adicValuation_ne_inftyValuation

added theorem RatFunc.adicValuation_not_isEquiv_infty_valuation

added theorem RatFunc.exists_zpow_uniformizingPolynomial

added theorem RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero

added theorem RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty

added theorem RatFunc.uniformizingPolynomial_isUniformizer

added theorem RatFunc.uniformizingPolynomial_ne_zero

added def RatFunc.valuationIdeal

added theorem RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X

added theorem RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one

added theorem RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty

added theorem RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one

added theorem RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X

added theorem RatFunc.valuation_isEquiv_infty_or_adic

added theorem RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one

added theorem RatFunc.valuation_uniformizingPolynomial_lt_one

Modified docs/1000.yaml