The executable-Vector ↔ Mathlib-Fin n → R equivalence, the fold-to-Finset.sum bridge for dot products, and the matrix-vector-product correspondence.

These are the base facts through which the row-span, rank, and nullspace bridges (in HexRowReduceMathlib) and the lattice bridges (in HexLLLMathlib) move between the two vector representations.

def HexMatrixMathlib.vectorEquiv {R : Type u} {n : ℕ} : Vector R n ≃ (Fin n → R)

Convert an executable Vector into Mathlib's function representation.

Equations

• HexMatrixMathlib.vectorEquiv = { toFun := fun (v : Vector R n) (i : Fin n) => v[i], invFun := Vector.ofFn, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem HexMatrixMathlib.vectorEquiv_apply {R : Type u} {n : ℕ} (v : Vector R n) (i : Fin n) : vectorEquiv v i = v[i]

vectorEquiv v has entry v[i] at i, so a caller can rewrite vectorEquiv v i to v[i] without unfolding it.

@[simp]

theorem HexMatrixMathlib.vectorEquiv_symm_apply {R : Type u} {n : ℕ} (f : Fin n → R) (i : Fin n) : (vectorEquiv.symm f)[↑i] = f i

The inverse direction of vectorEquiv materialises a function as an executable vector entrywise: (vectorEquiv.symm f)[i] is just f i.

theorem HexMatrixMathlib.foldl_finRange_eq_sum {R : Type u} {n : ℕ} [AddCommMonoid R] (f : Fin n → R) : List.foldl (fun (acc : R) (i : Fin n) => acc + f i) 0 (List.finRange n) = ∑ i : Fin n, f i

A left fold of (· + f ·) over List.finRange n from 0 is the finite sum ∑ i, f i; the bridge from the executable fold-sum to Mathlib's Finset.sum.

theorem HexMatrixMathlib.dotProduct_eq {R : Type u} {n : ℕ} [NonUnitalNonAssocSemiring R] (u v : Vector R n) : u.dotProduct v = vectorEquiv u ⬝ᵥ vectorEquiv v

The executable dot product equals Mathlib's dotProduct of the two vectors read through vectorEquiv.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_row {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) (i : Fin n) : (matrixEquiv M).row i = vectorEquiv (M.row i)

Row i of the Mathlib matrix matrixEquiv M is the image under vectorEquiv of the executable row Hex.Matrix.row M i, letting span/rank lemmas pass between the two row representations.

@[simp]

theorem HexMatrixMathlib.matrixEquiv_col {R : Type u} {n m : ℕ} (M : Hex.Matrix R n m) (j : Fin m) : (matrixEquiv M).col j = vectorEquiv (M.col j)

Column j of the Mathlib matrix matrixEquiv M is the image under vectorEquiv of the executable column Hex.Matrix.col M j.

theorem HexMatrixMathlib.vectorEquiv_mulVec {R : Type u} {n m : ℕ} [Semiring R] (M : Hex.Matrix R n m) (v : Vector R m) : vectorEquiv (M * v) = (matrixEquiv M).mulVec (vectorEquiv v)

The executable matrix-vector product transports to Mathlib's Matrix.mulVec under matrixEquiv/vectorEquiv.