def Hex.Matrix.independent {n m : Nat} (b : Matrix Int n m) : Prop

The rows of b are linearly independent, witnessed by positivity of each executable leading Gram determinant.

Equations

• b.independent = Hex.GramSchmidt.Int.independent b

@[instance_reducible]

instance Hex.Matrix.instDecidableIndependent {n m : Nat} (b : Matrix Int n m) : Decidable b.independent

Independence is decidable (via GramSchmidt.Int.independent), so it can be tested at runtime.

Equations

• b.instDecidableIndependent = Hex.Matrix.instDecidableIndependent._aux_1 b

theorem Hex.Internal.memLattice_of_rowSwap_memLattice {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (v : Vector Int m) : (b.rowSwap i j).memLattice v → b.memLattice v

memLattice_of_rowSwap_memLattice states that any vector in the lattice generated by rowSwap b i j also lies in the lattice generated by b.

theorem Hex.Internal.rowSwap_memLattice_iff {n m : Nat} (b : Matrix Int n m) (i j : Fin n) (v : Vector Int m) : (b.rowSwap i j).memLattice v ↔ b.memLattice v

rowSwap_memLattice_iff states that swapping rows i and j of b preserves lattice membership in both directions.

theorem Hex.Internal.memLattice_of_rowAdd_memLattice {n m : Nat} (b : Matrix Int n m) (src dst : Fin n) (c : Int) (v : Vector Int m) : (b.rowAdd src dst c).memLattice v → b.memLattice v

memLattice_of_rowAdd_memLattice states that any vector in the lattice generated by rowAdd b src dst c also lies in the lattice generated by b.

theorem Hex.Internal.rowAdd_memLattice_iff {n m : Nat} (b : Matrix Int n m) {src dst : Fin n} (hne : src ≠ dst) (c : Int) (v : Vector Int m) : (b.rowAdd src dst c).memLattice v ↔ b.memLattice v

rowAdd_memLattice_iff states that adding c times row src to a distinct row dst of b preserves lattice membership in both directions.