refactor: change definition of restricted power series to align with restricted multivariate power series#39583

WilliamCoram wants to merge 6 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

WilliamCoram:RestrictedPSWilliamCoram/mathlib4:RestrictedPSCopy head branch name to clipboard