feat(RingTheory/Powerseries): Weierstrass preparation for complete local ring

[Thmoas-Guan]

Weierstrass preparation theorem for complete local ring

---

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

[github-actions]

PR summary b097aebb18

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
+ 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]

I extracted a common part of two proofs as PowerSeries.order_eq_of_eq_zero_iff, where do we expext to put this lemma?

[acmepjz]

I extracted a common part of two proofs as PowerSeries.order_eq_of_eq_zero_iff, where do we expext to put this lemma?

This lemma seems a bit ad-hoc IMHO... If you really need it then it definitely should go to the file where the PowerSeries.order is defined.

BTW do you think the following proof is better?

lemma PowerSeries.order_eq_of_eq_zero_iff {R S : Type*} [Semiring R] [Semiring S]
    {φ : PowerSeries R} {ψ : PowerSeries S} (h : ∀ i, coeff _ i φ = 0 ↔ coeff _ i ψ = 0) :
    φ.order = ψ.order := by
  have : φ = 0 ↔ ψ = 0 := by simp_rw [PowerSeries.ext_iff, map_zero, h]
  simp_rw [order]
  congr!
  exact h _

[Thmoas-Guan]

I extracted a common part of two proofs as PowerSeries.order_eq_of_eq_zero_iff, where do we expext to put this lemma?

This lemma seems a bit ad-hoc IMHO... If you really need it then it definitely should go to the file where the PowerSeries.order is defined.

BTW do you think the following proof is better?

lemma PowerSeries.order_eq_of_eq_zero_iff {R S : Type*} [Semiring R] [Semiring S]
    {φ : PowerSeries R} {ψ : PowerSeries S} (h : ∀ i, coeff _ i φ = 0 ↔ coeff _ i ψ = 0) :
    φ.order = ψ.order := by
  have : φ = 0 ↔ ψ = 0 := by simp_rw [PowerSeries.ext_iff, map_zero, h]
  simp_rw [order]
  congr!
  exact h _

I think this proof is better.
I add this lemma just because I don't want to stuff everything inside the main proof.
Should I just mark this lemma PowerSeries.order_eq_of_eq_zero_iff private?

[acmepjz]

Should I just mark this lemma PowerSeries.order_eq_of_eq_zero_iff private?

I think this should be better.

[acmepjz]

After discussion with @Thmoas-Guan , we decided to replace the contents of close this PR and open a new PR by my solution at https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/RingTheory/PowerSeries/WeierstrassPreparation.lean.

[Thmoas-Guan]

This PR is replaced by the better setting of weierstrass division, thus closed. See #24584