Weierstrass preparation theorem for power series over a complete local ring

Already merged into mathlib.