Finite coefficient tensors and their algebraic transformations.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing {K : Type u_1} [CommSemiring K] (U : Type u_3) [DecidableEq U] : Tensor K U U Unit

The diagonal dot-pairing tensor, with a singleton third coordinate.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing U i j x✝ = if i = j then 1 else 0

@[simp]

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.dotPairing_matching {K : Type u_1} {U : Type u_2} [CommSemiring K] [DecidableEq U] (i : U) : dotPairing U i i () = 1

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.contract_dotPairing {K : Type u_1} {U : Type u_2} [CommSemiring K] [DecidableEq U] [Fintype U] (a b : U → K) : (dotPairing U).contract a b () = ∑ i : U, a i * b i