Theorem Finset.prod_eq_mul_prod_diff_singleton_of_mem

Modification history

2026-02-27 06:57
Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean
feat: generalize `prod_eq_mul_prod_diff_singleton` (#35482) …
Added Finset.prod_eq_mul_prod_diff_singleton_of_memView on Github →