Commit 2026-05-06 18:10 c315f04d

View on Github →

chore(Data/Finsupp): make support_single simp (#38860) ... for throth Finsupp, DFinsupp and SkewMonoidAlgebra, and rename the first two from support_single_ne_zero.

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Algebra/Module/LinearMap/Polynomial.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/MonoidAlgebra/Grading.lean

Modified Mathlib/Algebra/MonoidAlgebra/Support.lean

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Support.lean

added theorem SkewMonoidAlgebra.support_single

deleted theorem SkewMonoidAlgebra.support_single_ne_zero

Modified Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean

Modified Mathlib/Data/DFinsupp/BigOperators.lean

Modified Mathlib/Data/DFinsupp/Defs.lean

added theorem DFinsupp.support_single

deleted theorem DFinsupp.support_single_ne_zero

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/Multiset.lean

Modified Mathlib/Data/Finsupp/Order.lean

Modified Mathlib/Data/Finsupp/Single.lean

added theorem Finsupp.support_single

deleted theorem Finsupp.support_single_ne_zero

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

Modified Mathlib/LinearAlgebra/Finsupp/Supported.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean

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

Modified Mathlib/RingTheory/MvPowerSeries/Rename.lean