feat(RingTheory/PowerSeries/WeierstrassPreparation): add algebra isomorphisms induced by Weierstrass division (#25087)

- a distinguished polynomial `g` induces a natural isomorphism `A[X] / (g) ≃ A⟦X⟧ / (g)`
- a Weierstrass factorization `g = f * h` induces a natural isomorphism `A[X] / (f) ≃ A⟦X⟧ / (g)`

Author: acmepjz

Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Riccardo Brasca. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
+import Mathlib.RingTheory.Ideal.BigOperators
 import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
 import Mathlib.RingTheory.Polynomial.ScaleRoots
 
@@ -56,14 +57,29 @@ namespace IsWeaklyEisensteinAt
 
 section CommSemiring
 
-variable [CommSemiring R] {𝓟 : Ideal R} {f : R[X]}
+variable [CommSemiring R] {𝓟 : Ideal R} {f f' : R[X]}
 
 theorem map (hf : f.IsWeaklyEisensteinAt 𝓟) {A : Type v} [CommSemiring A] (φ : R →+* A) :
     (f.map φ).IsWeaklyEisensteinAt (𝓟.map φ) := by
   refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_
   rw [coeff_map]
   exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))
 
+theorem mul (hf : f.IsWeaklyEisensteinAt 𝓟) (hf' : f'.IsWeaklyEisensteinAt 𝓟) :
+    (f * f').IsWeaklyEisensteinAt 𝓟 := by
+  rw [isWeaklyEisensteinAt_iff] at hf hf' ⊢
+  intro n hn
+  rw [coeff_mul]
+  refine sum_mem _ fun x hx ↦ ?_
+  rcases lt_or_le x.1 f.natDegree with hx1 | hx1
+  · exact mul_mem_right _ _ (hf hx1)
+  replace hx1 : x.2 < f'.natDegree := by
+    by_contra!
+    rw [HasAntidiagonal.mem_antidiagonal] at hx
+    replace hn := hn.trans_le natDegree_mul_le
+    linarith
+  exact mul_mem_left _ _ (hf' hx1)
+
 end CommSemiring
 
 section CommRing

Mathlib/RingTheory/Polynomial/Eisenstein/Distinguished.lean

@@ -31,6 +31,10 @@ structure Polynomial.IsDistinguishedAt (f : R[X]) (I : Ideal R) : Prop
 
 namespace Polynomial.IsDistinguishedAt
 
+lemma mul {f f' : R[X]} {I : Ideal R} (hf : f.IsDistinguishedAt I) (hf' : f'.IsDistinguishedAt I) :
+    (f * f').IsDistinguishedAt I :=
+  ⟨hf.toIsWeaklyEisensteinAt.mul hf'.toIsWeaklyEisensteinAt, hf.monic.mul hf'.monic⟩
+
 lemma map_eq_X_pow {f : R[X]} {I : Ideal R} (distinguish : f.IsDistinguishedAt I) :
     f.map (Ideal.Quotient.mk I) = Polynomial.X ^ f.natDegree := by
   ext i