Theorem Finset.prod_extend

Modification history

2026-10-06 21:24
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
feat(Algebra/BigOperators): prod/sum of Function.extend (#44362) …
Added Finset.prod_extendView on Github →