Commit 2024-07-18 07:43 03c60116

View on Github →

feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series (#14418) Add some properties conneccting the $X$-adic valuation of a Laurent series to the vanishing of its coefficients, together with explicit values of the valuation of some basic Laurent series.

depends on: #13064

Estimated changes

Modified Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

added theorem Polynomial.valuation_of_mk

Modified Mathlib/FieldTheory/RatFunc/Basic.lean

added theorem RatFunc.mk_eq_mk'

Modified Mathlib/RingTheory/LaurentSeries.lean

added theorem LaurentSeries.coeff_zero_of_lt_intValuation

added theorem LaurentSeries.coeff_zero_of_lt_valuation

added theorem LaurentSeries.eq_coeff_of_valuation_sub_lt

added theorem LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero

added theorem LaurentSeries.val_le_one_iff_eq_coe

added theorem LaurentSeries.valuation_X_pow

added theorem LaurentSeries.valuation_le_iff_coeff_lt_eq_zero

added theorem LaurentSeries.valuation_single_zpow

added theorem RatFunc.valuation_eq_LaurentSeries_valuation