Commit 2025-12-08 03:11 6201e59c

View on Github →

feat: replace Finsupp.embDomain_apply with more general lemma (#31929)

depends on #31927
depends on #31928

Estimated changes

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

Modified Mathlib/Algebra/Polynomial/Reverse.lean

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/Defs.lean

modified theorem Finsupp.embDomain_apply

added theorem Finsupp.embDomain_apply_self

Modified Mathlib/Data/Finsupp/Option.lean

Modified Mathlib/Data/Finsupp/Sigma.lean

Modified Mathlib/Data/Finsupp/Single.lean

Modified Mathlib/Data/List/ToFinsupp.lean