Theorem MvPowerSeries.isRestricted_abs_iff

Modification history

2026-06-29 09:26
Mathlib/RingTheory/MvPowerSeries/Restricted.lean
feat: define multivariate restricted power series (#32692) …
Added MvPowerSeries.isRestricted_abs_iffView on Github →