Commit 2025-05-18 15:21 e1e23a5d

feat(RingTheory/PowerSeries/WeierstrassPreparation): Weierstrass division over complete local ring (#24935) We define Weierstrass division, which is a preliminary work towards to Weierstrass preparation theorem (#24584). We assume that a ring is adic complete with respect to some ideal. If such ideal is a maximal ideal, then by isLocalRing_of_isAdicComplete_maximal, such ring has only on maximal ideal, and hence such ring is a complete local ring.

Main definitions

• PowerSeries.IsWeierstrassDivisionAt f g q r I: a Prop which asserts that a power series q and a polynomial r of degree < n satisfy f = g * q + r, where n is the order of the image of g in (A / I)⟦X⟧ (defined to be zero if such image is zero, in which case it's mathematically not considered).
• PowerSeries.IsWeierstrassDivision: version of PowerSeries.IsWeierstrassDivisionAt for local rings with respect to its maximal ideal.

Main results

• PowerSeries.exists_isWeierstrassDivision: Weierstrass division: let f, g be power series over a complete local ring, such that the image of g in the residue field is not zero. Let n be the order of the image of g in the residue field. Then there exists a power series q and a polynomial r of degree < n, such that f = g * q + r.
• PowerSeries.IsWeierstrassDivision.elim: The q and r in the Weierstrass division is unique.