11.6. Worked example🔗

The block builds an integer matrix with the #m[...] literal and checks the squared norm of the first row (2² + 0² + 1² = 5), the dot product of the first two rows (4), that the identity fixes a vector, and one elementary row operation: adding row 0 to row 2 (rowAdd A 0 2 1) replaces row 2 = (0, 1, 1) with (0, 1, 1) + (2, 0, 1) = (2, 1, 2).

open Hex

namespace HexMatrixChapterExample

def A : Matrix Int 3 3 := #m[2, 0, 1; 1, 3, 2; 0, 1, 1]

#guard (A.row 0).normSq = 5

#guard (A.row 0).dotProduct (A.row 1) = 4

def v : Vector Int 3 := #v[1, 2, 3]

#guard (Matrix.identity (R := Int) 3).mulVec v = v

#guard (Matrix.rowAdd A 0 2 1).row 2 = #v[2, 1, 2]

end HexMatrixChapterExample