Theorem PowerSeries.IsRestricted.isRestricted_iff_abs

Modification history

2025-09-22 13:29
Mathlib/RingTheory/PowerSeries/Restricted.lean
feat: restricted power series form a ring (#26089) …
Added PowerSeries.IsRestricted.isRestricted_iff_absView on Github →