Commit 2026-03-11 00:43 a19d30d2

View on Github →

feat(RingTheory/MvPowerSeries): introduce rename (#33188) This file establishes the rename operation on multivariate power series under a map with finite fibers, which modifies the set of variables. This file is patterned after 'Mathlib/Algebra/MvPolynomial/Rename.lean`

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finsupp/Antidiagonal.lean

added theorem Finsupp.image_prodMap_embDomain_antidiagonal

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.embDomain_trans_apply

added theorem Finsupp.mapDomain_apply_eq_sum

added theorem Finsupp.mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits

added theorem Finsupp.mapDomain_support_of_subsingletonAddUnits

added theorem Finsupp.mem_range_embDomain_iff

Modified Mathlib/Data/Finsupp/Defs.lean

added theorem Finsupp.embDomain_refl

Modified Mathlib/Data/Finsupp/Order.lean

added theorem Finsupp.isLowerSet_range_embDomain

Modified Mathlib/Data/Finsupp/Weight.lean

added theorem Finsupp.degree_comapDomain_le_of_canonicallyOrderedAdd

added theorem Finsupp.degree_mapDomain_eq_of_subsingletonAddUnits

Created Mathlib/Order/Filter/TendstoCofinite.lean

added theorem Filter.TendstoCofinite.comp

added theorem Filter.TendstoCofinite.embedding

added theorem Filter.TendstoCofinite.equiv

added theorem Filter.TendstoCofinite.finite_preimage

added theorem Filter.TendstoCofinite.finite_preimage_singleton

added theorem Filter.TendstoCofinite.id

added theorem Filter.TendstoCofinite.mapDomain_add

added theorem Filter.TendstoCofinite.mapDomain_eq_zero

added theorem Filter.TendstoCofinite.mapDomain_smul

added theorem Filter.tendstoCofinite_iff_finite_preimage_singleton

added theorem Filter.tendstoCofinite_of_finite

added theorem Filter.tendstoCofinite_of_injective

added theorem Finsupp.mapDomain_tendstoCofinite

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

modified theorem MvPowerSeries.X_def

Created Mathlib/RingTheory/MvPowerSeries/Rename.lean

added theorem MvPowerSeries.coeff_embDomain_rename

added theorem MvPowerSeries.coeff_killCompl

added theorem MvPowerSeries.coeff_rename

added theorem MvPowerSeries.coeff_rename_eq_zero

added theorem MvPowerSeries.constantCoeff_rename

added def MvPowerSeries.killCompl

added def MvPowerSeries.killComplFun

added theorem MvPowerSeries.killCompl_C

added theorem MvPowerSeries.killCompl_X

added theorem MvPowerSeries.killCompl_X_eq_zero

added theorem MvPowerSeries.killCompl_comp_rename

added theorem MvPowerSeries.killCompl_map

added theorem MvPowerSeries.killCompl_monomial_embDomain

added theorem MvPowerSeries.killCompl_monomial_eq_zero

added theorem MvPowerSeries.killCompl_rename_app

added def MvPowerSeries.rename

added def MvPowerSeries.renameEquiv

added theorem MvPowerSeries.renameEquiv_refl

added theorem MvPowerSeries.renameEquiv_symm

added theorem MvPowerSeries.renameEquiv_trans

added def MvPowerSeries.renameFun

added theorem MvPowerSeries.rename_C

added theorem MvPowerSeries.rename_X

added theorem MvPowerSeries.rename_coe

added theorem MvPowerSeries.rename_comp_rename

added theorem MvPowerSeries.rename_id

added theorem MvPowerSeries.rename_id_apply

added theorem MvPowerSeries.rename_inj

added theorem MvPowerSeries.rename_injective

added theorem MvPowerSeries.rename_map

added theorem MvPowerSeries.rename_monomial

added theorem MvPowerSeries.rename_rename