Multiplication in coordinates: definition

Let K be an algebra over F with a basis b = (b 0, …, b (n - 1)). Multiplication in K, written in coordinates, is the map fieldMul b : F ^ (n + n) → F ^ n sending the coordinates x and y of two elements to the coordinates of their product: fieldMul b (x, y) = b.repr ((∑ i, x i • b i) * ∑ j, y j • b j). The first n inputs (Fin.castAdd n i) are the coordinates of the first factor and the last n inputs (Fin.natAdd n j) those of the second; Fin.append x y is the input (x, y). For a finite field K of degree n over F this is multiplication in the extension of degree n, for example in GF(2 ^ n) over GF(2).

noncomputable def Algebraic.Cutwidth.MultiOutput.fieldMul {n : ℕ} {F : Type u_1} {K : Type u_2} [CommSemiring F] [Semiring K] [Algebra F K] (b : Module.Basis (Fin n) F K) (z : Fin (n + n) → F) : Fin n → F

Multiplication in coordinates. For a basis b of K over F indexed by Fin n, the map sending the coordinates of x (the first n inputs) and of y (the last n inputs) to the coordinates of x * y.

Equations

• Algebraic.Cutwidth.MultiOutput.fieldMul b z i = (b.repr ((∑ j : Fin n, z (Fin.castAdd n j) • b j) * ∑ j : Fin n, z (Fin.natAdd n j) • b j)) i