Commit 2026-09-04 14:00 47e86e9f

refactor(RatFunc/Ostrowski): drop unnecessary hypothesis (#43249) Ostrowski's theorem for k(X) states that a nontrivial valuation v which is trivial on the base field k is either equivalent to the valuation at infinity or to the p-adic valuation for a unique maximal ideal p of K[X]. See here for the source. What is currently in mathlib: A rank one discrete valuation v which is ... (rest is same as above) What this PR proposes: A nontrivial v which is ... (rest is same as above) The rank one discrete hypothesis is strictly stronger than what is required here. Any user wanting to apply this lemma needs to discharge this by proving IsRankOneDiscrete v for their specific valuation. Note: A nontrivial valuation on k(X) can be shown to be rank one discrete. It is essentially immediate from Ostrowski since the valuation at infinity and the p-adics are already rank one discrete in Mathlib. We are, however, missing some API to prove this easily: A valuation equiv. to a rank one discrete valuation is rank one discrete. This fact should not be an assumption but a theorem. AI disclaimer: I asked Claude Fable to draft a correct proof of valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one with the current hypotheses.