Reindexing a product by a symmetric difference

In a generalized Boolean algebra b ↦ a ∆ b is an involution, so over a finite generalized Boolean algebra the product of f (a ∆ b) over all b is the product of f b over all b (Fintype.prod_symmDiff, Fintype.sum_symmDiff). The main instance is the Boolean algebra of the subsets of a finite type, where this reindexes sums over sets of coordinates by S ↦ T ∆ S.

Main results

• Fintype.prod_symmDiff, Fintype.sum_symmDiff: reindexing a product or a sum by a symmetric difference.

theorem Fintype.prod_symmDiff {α : Type u_1} {M : Type u_2} [Fintype α] [GeneralizedBooleanAlgebra α] [CommMonoid M] (a : α) (f : α → M) : ∏ b : α, f (symmDiff a b) = ∏ b : α, f b

Reindexing a product over a finite generalized Boolean algebra by the involution b ↦ a ∆ b.

theorem Fintype.sum_symmDiff {α : Type u_1} {M : Type u_2} [Fintype α] [GeneralizedBooleanAlgebra α] [AddCommMonoid M] (a : α) (f : α → M) : ∑ b : α, f (symmDiff a b) = ∑ b : α, f b

Reindexing a sum over a finite generalized Boolean algebra by the involution b ↦ a ∆ b.