Commit 2026-10-06 21:24 f2273d05

View on Github →

feat(Algebra/BigOperators): prod/sum of Function.extend (#44362) This generalizes the existing Finset.prod_eq_prod_extend from Subtype.val to an arbitrary function. I flipped the direction to make RHS the simpler form.

Estimated changes

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

modified theorem Finset.prod_eq_prod_extend

added theorem Finset.prod_extend

added theorem Finset.prod_extend_one

added theorem Finset.prod_extend_one_of_injective