Disjoint affine cubes

A cube is specified by a base point and binary direction vectors. The directions are disjoint if each original coordinate is changed by at most one direction.

def Algebraic.BooleanCube.ModThree.DisjointDirections {ι : Type u_1} {J : Type u_2} (v : J → ι → ZMod 2) : Prop

At each coordinate, at most one direction is nonzero.

Equations

• Algebraic.BooleanCube.ModThree.DisjointDirections v = ∀ (j k : J), j ≠ k → ∀ (i : ι), v j i = 0 ∨ v k i = 0

def Algebraic.BooleanCube.ModThree.cubeLinearMap {ι : Type u_1} {J : Type u_2} [Fintype J] (v : J → ι → ZMod 2) : (J → ZMod 2) →ₗ[ZMod 2] ι → ZMod 2

The linear part of an affine cube specified by direction vectors.

Equations

• Algebraic.BooleanCube.ModThree.cubeLinearMap v = { toFun := fun (z : J → ZMod 2) => ∑ j : J, z j • v j, map_add' := ⋯, map_smul' := ⋯ }

def Algebraic.BooleanCube.ModThree.affineCube {ι : Type u_1} {J : Type u_2} [Fintype J] (a : ι → ZMod 2) (v : J → ι → ZMod 2) (z : J → ZMod 2) : ι → ZMod 2

The affine cube obtained by independently selecting direction vectors.

Equations

• Algebraic.BooleanCube.ModThree.affineCube a v z = a + (Algebraic.BooleanCube.ModThree.cubeLinearMap v) z