feat(RingTheory/Powerseries): Weierstrass preparation

[Thmoas-Guan]

Weierstrass preparation for complete DVR.

---

• depends on: [Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900
• depends on: feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring #21944
• depends on: [Merged by Bors] - feat(RingTheory):Add lemma about factorPow #22369

[github-actions]

PR summary 6c8ac7478d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.WeierstrassPreparation (new file)	1337

---

Declarations diff

+ CompleteLocalRing.weierstrass_preparation
+ IsDiscreteValuationRing.weierstrass_preparation
+ IsDiscreteValuationRing.weierstrass_preparation_aux
+ PowerSeries.order_eq_of_eq_zero_iff
+ map_ne_top
+ preparation_lift
+ preparation_lift_triv

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Thmoas-Guan]

There are a lot of lemmas twisted together, I may need some help to decompose this PR, thank for the helps.

[riccardobrasca]

This PR is huge, is it possible to split it? For example, the first result can go in another file and you open a PR with prerequisites for the main theorem. Anyway thanks a lot, we surely want this!

[Thmoas-Guan]

This PR is huge, is it possible to split it? For example, the first result can go in another file and you open a PR with prerequisites for the main theorem. Anyway thanks a lot, we surely want this!

The problem is, the things after the complete local ring version doesn't take long, however it can reduce the lenth for about 100 to 150 lines. However I don't clearly know where should the first result go.
There are still a lot of part of this needing refinement. Thanks a lot if you can help.

[riccardobrasca]

I am still looking only at the first lemma, and we actually already have it. It is basically Polynomial.lifts_and_degree_eq_and_monic

[riccardobrasca]

This is also defined in #21582 (if I am not confused). @jjdishere can you confirm?

[jjdishere]

Yes, and this is more general than the definition R⧸m ^ (n + 1) →+* R⧸m ^ n in #21582 .

[Thmoas-Guan]

I am still looking only at the first lemma, and we actually already have it. It is basically Polynomial.lifts_and_degree_eq_and_monic

Sorry, my fault, I don't know why aesop didn't return me this.

[jjdishere]

I've discussed with @Thmoas-Guan about the intersection part of this PR and #21582 . He will try to split out the common part of this and #21582 into a new PR.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(RingTheory/Ideal/Quotient): define transtition map between ring or module quotient by powers of ideal #21900
• feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring #21944
• [Merged by Bors] - feat(RingTheory):Add lemma about factorPow #22369
  By Dependent Issues (🤖). Happy coding!

[Thmoas-Guan]

This PR is replaced by the better setting of weierstrass division, thus closed. Would be developed soon based on #24584