Commit 2026-09-09 15:18 2e52d79f

View on Github →

feat(Data/Finsupp): support of mapDomain is image of support if nonneg (#43610) Also replace MulLeftMono by IsOrderedMonoid in a bunch of lemmas about commutative monoids, since the latter is mathematically equivalent but stronger according to TC search.

Moves

Finsupp.mapDomain_apply -> Finsupp.mapDomain_apply_of_injective to make space for the more general lemma that doesn't assume injectivity.

Estimated changes

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

modified theorem Finset.exists_lt_of_prod_lt

modified theorem Finset.exists_lt_one_of_prod_one_of_exists_ne_one

modified theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Data/Finsupp/Basic.lean

modified def Finsupp.mapDomain

modified theorem Finsupp.mapDomain_apply

added theorem Finsupp.mapDomain_apply_of_injective

added theorem Finsupp.prod_comapDomain

deleted theorem Finsupp.sum_comapDomain

Modified Mathlib/Data/Finsupp/Order.lean

added theorem Finsupp.support_mapDomain_of_nonneg

Modified Mathlib/Data/Finsupp/SMul.lean

Modified Mathlib/RepresentationTheory/Basic.lean

Modified Mathlib/RingTheory/Extension/Generators.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean