feat(RingTheory/LaurentSeries): add properties of the X-adic valuation on Laurent series

[faenuccio]

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.

Co-authored-by: María Inés de Frutos-Fernández @mariainesdff

• [ ] depends on: #13064

[github-actions[bot]]

PR summary 2712d2d6dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coeff_zero_of_lt_intValuation + coeff_zero_of_lt_valuation + eq_coeff_of_valuation_sub_lt + instance : Valued (LaurentSeries K) ℤₘ₀ := Valued.mk' (PowerSeries.idealX K).valuation + intValuation_le_iff_coeff_lt_eq_zero + mk_eq_mk' + val_le_one_iff_eq_coe + valuation_X_pow + valuation_eq_LaurentSeries_valuation + valuation_le_iff_coeff_lt_eq_zero + valuation_of_mk + valuation_single_zpow

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[ScottCarnahan]

Have you considered using AddVal from Mathlib.RingTheory.HahnSeries.Summable? It looks like the order API from Hahn series can make some of your proofs shorter.

[faenuccio]

Have you considered using AddVal from Mathlib.RingTheory.HahnSeries.Summable? It looks like the order API from Hahn series can make some of your proofs shorter.

Oh no, I had briefly had a look and then decided that since I was going for a MulVal they were unrelated. I will check it and try to simply my proofs - thanks!

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13064~~ By Dependent Issues (🤖). Happy coding!

[faenuccio]

Have you considered using AddVal from Mathlib.RingTheory.HahnSeries.Summable? It looks like the order API from Hahn series can make some of your proofs shorter.

@ScottCarnahan I have had a look but it seems to me that since most of the material about AddVal concerns... additive valuations, there is not much I can gain: I would at any rate need to set-up a dictionary. Or am I missing something, do you have explicit instances in mind where this could help?

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style