def Hex.Matrix.memLattice {n m : Nat} (b : Matrix Int n m) (v : Vector Int m) : Prop

v lies in the integer lattice generated by the rows of b.

Equations

• b.memLattice v = ∃ (c : Vector Int n), Hex.Matrix.vecMul c b = v

theorem Hex.Matrix.vecMul_sub {n m : Nat} (c d : Vector Int n) (B : Matrix Int n m) : vecMul (c - d) B = vecMul c B - vecMul d B

Row combinations preserve subtraction of coefficient vectors.

theorem Hex.Matrix.vecMul_unit {n m : Nat} (B : Matrix Int n m) (i : Fin n) : vecMul (Vector.unit Int i) B = B[i]

A unit coefficient vector selects the corresponding matrix row.

theorem Hex.Matrix.row_memLattice {n m : Nat} (B : Matrix Int n m) (i : Fin n) : B.memLattice B[i]

Every row of a matrix belongs to its integer row lattice.

theorem Hex.Matrix.memLattice_sub {n m : Nat} {B : Matrix Int n m} {u v : Vector Int m} (hu : B.memLattice u) (hv : B.memLattice v) : B.memLattice (u - v)

Integer row lattices are closed under subtraction.

theorem Hex.Matrix.memLattice_smul {n m : Nat} {B : Matrix Int n m} {v : Vector Int m} (a : Int) (hv : B.memLattice v) : B.memLattice (a • v)

Integer row lattices are closed under integer scalar multiplication.

theorem Hex.Matrix.vecMul_transpose_mul {n' n m : Nat} (U : Matrix Int n' n) (B : Matrix Int n m) (c : Vector Int n') : vecMul (U.transpose * c) B = vecMul c (U * B)

Row combinations transport across an explicit integer row transform.

theorem Hex.Matrix.memLattice_of_mul_eq {n m n' : Nat} {B : Matrix Int n m} {B' : Matrix Int n' m} {U : Matrix Int n' n} {v : Vector Int m} (h : U * B = B') : B'.memLattice v → B.memLattice v

If every row of B' is an integer row combination of rows of B, then membership in the lattice generated by B' implies membership for B.

theorem Hex.Matrix.memLattice_iff_of_mul_eq {n m : Nat} {B B' : Matrix Int n m} {U V : Matrix Int n n} (hU : U * B = B') (hV : V * B' = B) (v : Vector Int m) : B.memLattice v ↔ B'.memLattice v

Two explicit integer row transforms in opposite directions prove equality of the generated row lattices.