Commit 2026-01-26 09:39 8c557f96

View on Github →

feat: lemmas about symmDiff and finite sums (#34410) Convenience lemmas cherry picked from #34055

Estimated changes

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

added theorem Finset.prod_biUnion_of_pairwise_eq_one

Modified Mathlib/Data/Set/SymmDiff.lean

modified theorem Set.mem_symmDiff

added theorem Set.symmDiff_union_subset

added theorem Set.union_symmDiff_subset

added theorem Set.union_symmDiff_union_subset