Theorem Finset.prod_extend_one_of_injective

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_extend_one_of_injective View on Github →