Commit 2024-06-25 00:00 3dce761d

View on Github →

feat(RingTheory/MvPolynomial): multivariate polynomials preserve localization (#14055) If S is the localization of R at a submonoid M, then MvPolynomial σ S is the localization of MvPolynomial σ R at the image of M in MvPolynomial σ R.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

added theorem Finsupp.prod_mul_eq_prod_mul_of_exists

Modified Mathlib/Algebra/BigOperators/Group/Finset.lean

added theorem Finset.prod_mul_eq_prod_mul_of_exists

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

modified theorem MvPolynomial.algHom_C

Modified Mathlib/Algebra/MvPolynomial/Counit.lean

Modified Mathlib/RingTheory/Generators.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

added theorem MvPolynomial.algebraMap_def

Created Mathlib/RingTheory/MvPolynomial/Localization.lean

added theorem MvPolynomial.isLocalization_C_mk'

Modified Mathlib/RingTheory/WittVector/WittPolynomial.lean