The matrix multiplication tensor over an arbitrary coefficient semiring

Tensor.matrixMultiplication is stated over ℂ; the all-fields development uses this field-generic copy, which is definitionally the same tensor.

def MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matMul (K : Type u_1) [CommSemiring K] (a b c : ℕ) : Tensor K (Fin a × Fin b) (Fin b × Fin c) (Fin c × Fin a)

The ⟨a,b,c⟩ matrix multiplication tensor over an arbitrary commutative semiring (the field-generic form of Tensor.matrixMultiplication).

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matMul K a b c x y z = if x.2 = y.1 ∧ y.2 = z.1 ∧ z.2 = x.1 then 1 else 0

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matMul_eq_matrixCoefficients (K : Type u_1) [CommSemiring K] (a b c : ℕ) : matMul K a b c = matrixCoefficients (Fin a) (Fin b) (Fin c)

theorem MatrixMultiplicationAllFields.MatrixMultiplication.Foundation.Tensor.matrixMultiplication_eq_matMul (a b c : ℕ) : matrixMultiplication a b c = matMul ℂ a b c