Matrix multiplication in coordinates: definition

The product C = A B of two n × n matrices, as a map with 2 n² inputs and n² outputs. The input coordinates are Fin (n * n + n * n): the entry A i j of the first factor sits at matMulLeft n i j, among the first n * n coordinates, and the entry B j k of the second factor at matMulRight n j k, among the last n * n. The output C i k sits at matMulOutput n i k. Pairs of indices are numbered row by row through finProdFinEquiv.

• matMul n z is the product read from the input z: output C i k is ∑ j, A i j * B j k.
• matMulInput A B is the input holding the two matrices A and B.
• matMulTermA n s, matMulTermB n s and matMulTermC out: the wires of a circuit with s gates and output wires out carrying the entries A i j, B j k and C i k, indexed by pairs of indices. These are the terminals.

def Algebraic.Cutwidth.MultiOutput.matMulLeft (n : ℕ) (i j : Fin n) : Fin (n * n + n * n)

The input coordinate of the entry A i j of the first factor.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulLeft n i j = Fin.castAdd (n * n) (finProdFinEquiv (i, j))

def Algebraic.Cutwidth.MultiOutput.matMulRight (n : ℕ) (j k : Fin n) : Fin (n * n + n * n)

The input coordinate of the entry B j k of the second factor.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulRight n j k = Fin.natAdd (n * n) (finProdFinEquiv (j, k))

def Algebraic.Cutwidth.MultiOutput.matMulOutput (n : ℕ) (i k : Fin n) : Fin (n * n)

The output coordinate of the entry C i k of the product.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulOutput n i k = finProdFinEquiv (i, k)

def Algebraic.Cutwidth.MultiOutput.matMul {R : Type u_1} [Semiring R] (n : ℕ) (z : Fin (n * n + n * n) → R) : Fin (n * n) → R

Matrix multiplication in coordinates. The output C i k is ∑ j, A i j * B j k, where A i j = z (matMulLeft n i j) and B j k = z (matMulRight n j k).

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.MultiOutput.matMulInput {R : Type u_1} {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) : Fin (n * n + n * n) → R

The input holding the matrices A and B.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.MultiOutput.matMulTermA (n s : ℕ) (q : Fin n × Fin n) : Wire (n * n + n * n) s

The wire of the input A i j.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulTermA n s q = Cslib.Circuits.Wire.input (Algebraic.Cutwidth.MultiOutput.matMulLeft n q.1 q.2)

def Algebraic.Cutwidth.MultiOutput.matMulTermB (n s : ℕ) (q : Fin n × Fin n) : Wire (n * n + n * n) s

The wire of the input B j k.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulTermB n s q = Cslib.Circuits.Wire.input (Algebraic.Cutwidth.MultiOutput.matMulRight n q.1 q.2)

def Algebraic.Cutwidth.MultiOutput.matMulTermC {n s : ℕ} (out : Fin (n * n) → Wire (n * n + n * n) s) (q : Fin n × Fin n) : Wire (n * n + n * n) s

The wire carrying the output C i k, among the output wires out.

Equations

• Algebraic.Cutwidth.MultiOutput.matMulTermC out q = out (Algebraic.Cutwidth.MultiOutput.matMulOutput n q.1 q.2)