Binary-field multiplication on Boolean inputs

For a binary field K with a basis b over the two-element field, multiplication in coordinates is MultiOutput.fieldMul b. Reading its 2n prime-field inputs and n outputs as Boolean bits gives a Boolean map on 2n inputs: the first n bits are the coordinates of x, the last n those of y, and the outputs are the coordinates of x * y.

noncomputable def Algebraic.Aggregate.Geometry.FieldMul.boolFieldMul {K : Type u_1} [Field K] [Algebra (ZMod 2) K] {n : ℕ} (b : Module.Basis (Fin n) (ZMod 2) K) (z : Fin (n + n) → Bool) : Fin n → Bool

Multiplication in a binary field with basis b, on 2n Boolean input bits.

Equations

• Algebraic.Aggregate.Geometry.FieldMul.boolFieldMul b z i = decide (Algebraic.Cutwidth.MultiOutput.fieldMul b (Algebraic.Aggregate.Geometry.bitVector z) i = 1)