Commit 2025-06-03 12:11 a48f6770

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)