Theorem PowerSeries.IsWeierstrassDivisorAt.eq_zero_of_mul_eq

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.IsWeierstrassDivisorAt.eq_zero_of_mul_eqView on Github →