Commit 2026-09-30 10:15 dca97ab9

View on Github →

feat: restricted multivariate power series as its own type and some missing API lemmas (#42867) We add some missing API lemmas for restricted multivariate power series, as well as promoting them to their own type MvPowerSeries.Restricted.

Estimated changes

Modified Mathlib/RingTheory/MvPowerSeries/Restricted.lean

added theorem MvPolynomial.isRestricted

added def MvPolynomial.toRestricted

added theorem MvPolynomial.toRestricted_C

added theorem MvPolynomial.toRestricted_X

added theorem MvPolynomial.toRestricted_eq_one_iff

added theorem MvPolynomial.toRestricted_eq_zero_iff

added theorem MvPolynomial.toRestricted_inj

added theorem MvPolynomial.toRestricted_injective

added theorem MvPolynomial.toRestricted_monomial

added theorem MvPolynomial.val_toRestricted

added theorem MvPowerSeries.IsRestricted.add

added theorem MvPowerSeries.IsRestricted.mem_addSubgroup

added theorem MvPowerSeries.IsRestricted.mem_subring

added theorem MvPowerSeries.IsRestricted.mul

added theorem MvPowerSeries.IsRestricted.neg

added theorem MvPowerSeries.IsRestricted.pow

added theorem MvPowerSeries.IsRestricted.smul

added theorem MvPowerSeries.IsRestricted.sub

added theorem MvPowerSeries.IsRestricted.sum

added def MvPowerSeries.Restricted.C

added def MvPowerSeries.Restricted.X

added theorem MvPowerSeries.Restricted.algebraMap_apply

added theorem MvPowerSeries.Restricted.coeff_val_mapAdditive

added theorem MvPowerSeries.Restricted.ext

added def MvPowerSeries.Restricted.map

added def MvPowerSeries.Restricted.mapAdditive

added theorem MvPowerSeries.Restricted.map_injective

added def MvPowerSeries.Restricted.monomial

added theorem MvPowerSeries.Restricted.val_C

added theorem MvPowerSeries.Restricted.val_X

added theorem MvPowerSeries.Restricted.val_add

added theorem MvPowerSeries.Restricted.val_map

added theorem MvPowerSeries.Restricted.val_monomial

added theorem MvPowerSeries.Restricted.val_mul

added theorem MvPowerSeries.Restricted.val_neg

added theorem MvPowerSeries.Restricted.val_one

added theorem MvPowerSeries.Restricted.val_pow

added theorem MvPowerSeries.Restricted.val_smul

added theorem MvPowerSeries.Restricted.val_sub

added theorem MvPowerSeries.Restricted.val_sum

added theorem MvPowerSeries.Restricted.val_zero

added def MvPowerSeries.Restricted

added theorem MvPowerSeries.isRestricted_X

added theorem MvPowerSeries.isRestricted_map

added theorem MvPowerSeries.isRestricted_of_finite_support

Modified Mathlib/RingTheory/PowerSeries/Restricted.lean