Theorem Finset.prod_biUnion_of_pairwise_eq_one

Modification history

2026-01-26 09:39
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
feat: lemmas about `symmDiff` and finite sums (#34410) …
Added Finset.prod_biUnion_of_pairwise_eq_oneView on Github →