Commit 2025-02-20 18:07 a1a75b3b

View on Github →

chore: rename some more Foo.sum_elim -> sumElim (#22130)

Estimated changes

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

added theorem Finset.prod_sumElim

deleted theorem Finset.prod_sum_elim

Modified Mathlib/Analysis/Convex/Combination.lean

Modified Mathlib/Data/Fintype/BigOperators.lean

added theorem Fintype.prod_sumElim

deleted theorem Fintype.prod_sum_elim

Modified Mathlib/Topology/LocallyFinite.lean

added theorem LocallyFinite.sumElim

deleted theorem LocallyFinite.sum_elim