Commit 2025-06-12 12:52 6763a6b9

View on Github →

chore(Data/Finset): rename disj_sum -> disjSum and disj_union -> disjUnion in lemmas (#25801) Renames four lemmas which do not follow the naming convention:

Finset.prod_disj_sum ->Finset.prod_disjSum
Finset.sum_disj_sum ->Finset.sum_disjSum
Finset.filter_disj_union ->Finset.filter_disjUnion
Finset.disj_sum_strictMono_right ->Finset.disjSum_strictMono_right

Estimated changes

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

added theorem Finset.prod_disjSum

deleted theorem Finset.prod_disj_sum

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.filter_disjUnion

deleted theorem Finset.filter_disj_union

Modified Mathlib/Data/Finset/Sum.lean

added theorem Finset.disjSum_strictMono_right

deleted theorem Finset.disj_sum_strictMono_right

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Fintype/BigOperators.lean