Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.groupTensor (G : Type u_1) [AddCommGroup G] [DecidableEq G] : Tensor ℂ G G G

The coefficient tensor for addition in a finite abelian group.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.groupTensor G a b c = if a + b = c then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.groupTensor_fourier (G : Type u_1) [AddCommGroup G] [Fintype G] [DecidableEq G] : groupTensor G = fun (a b c : G) => ∑ χ : AddChar G ℂ, Tensor.rankOne (fun (a : G) => χ a / ↑(Fintype.card G)) (fun (b : G) => χ b) (fun (c : G) => χ (-c)) a b c

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.groupTensor_rankAtMost (G : Type u_1) [AddCommGroup G] [Fintype G] [DecidableEq G] : (groupTensor G).RankAtMost (Fintype.card G)