Examples illustrating definitions elsewhere, to ease understanding and make definitions more concrete

def M : Matrix (Fin 3) (Fin 3) (ZMod 2)

Equations

• M = !![0, 1, 1; 0, 0, 0; 1, 1, 1]

def v : Fin 3 → ZMod 2

Equations

• v = ![1, 0, 1]

def Toeplitz2x3 (t1 t2 t3 t4 : ZMod 2) : Matrix (Fin 2) (Fin 3) (ZMod 2)

The most general binary 2x3 Toeplitz matrix

Equations

• Toeplitz2x3 t1 t2 t3 t4 = !![t1, t3, t4; t2, t1, t3]