Theorem PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem

Modification history

2025-06-03 12:11
Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean
feat(RingTheory/PowerSeries/WeierstrassPreparation): add algebra isomorphisms induced by Weierstrass division (#25087) …
Modified PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_memView on Github →
2025-05-18 15:21
Mathlib/RingTheory/PowerSeries/WeierstrassPreparation.lean
feat(RingTheory/PowerSeries/WeierstrassPreparation): Weierstrass division over complete local ring (#24935) …
Added PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_memView on Github →