Structure PowerSeries.IsWeierstrassDivisionAt

Modification history

2025-05-18 15:21

Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean

feat(RingTheory/PowerSeries/WeierstrassPreparation): Weierstrass division over complete local ring (#24935) …

Added PowerSeries.IsWeierstrassDivisionAt View on Github →