Commit 2025-12-15 11:03 02db42bc

View on Github →

chore(Data/Finsupp): rename the toFun projection to apply in simps (#32562) This is the standard name for fun-like types.

Estimated changes

Modified Counterexamples/CliffordAlgebraNotInjective.lean

Modified Mathlib/Algebra/Group/Finsupp.lean

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Finsupp/Interval.lean

Modified Mathlib/Data/Finsupp/Weight.lean

Modified Mathlib/LinearAlgebra/Dual/Basis.lean

modified theorem Module.Basis.toDual_range

Modified Mathlib/RingTheory/AlgebraTower.lean

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

Modified Mathlib/RingTheory/HahnSeries/HEval.lean