Theorems · Theorem · combinatorics

Finset.convolution.congr_simp

∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (A A_1 : Finset G),
  A = A_1 → ∀ (B B_1 : Finset G), B = B_1 → ∀ (a a_1 : G), a = a_1 → A.convolution B a = A_1.convolution B_1 a_1

Defined in

Mathlib.Combinatorics.Additive.Convolution

Cited by

4 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupDecidableEq