Hex.Matrix.rowSwap.{u_1} {R : Type u_1} {n m : ℕ} (M : Hex.Matrix R n m)
  (i j : Fin n) : Hex.Matrix R n m
Hex.Matrix.rowSwap.{u_1} {R : Type u_1}
  {n m : ℕ} (M : Hex.Matrix R n m)
  (i j : Fin n) : Hex.Matrix R n m

Swap rows i and j in a dense matrix.

Implemented with Vector.swap, which updates the dense backing store in place when M is uniquely referenced, rather than reading both rows and writing them back through two sets (which forces a copy of the outer vector).

Hex.Matrix.rowScale.{u_1} {R : Type u_1} {n m : ℕ} [Mul R]
  (M : Hex.Matrix R n m) (i : Fin n) (c : R) : Hex.Matrix R n m
Hex.Matrix.rowScale.{u_1} {R : Type u_1}
  {n m : ℕ} [Mul R] (M : Hex.Matrix R n m)
  (i : Fin n) (c : R) : Hex.Matrix R n m

Scale row i by c.

Vector.modify frees the row slot before applying the update, so when M is uniquely referenced both the outer vector and the row itself are updated in place: Vector.map reuses the freed row's backing store.

Hex.Matrix.rowAdd.{u_1} {R : Type u_1} {n m : ℕ} [Mul R] [Add R]
  (M : Hex.Matrix R n m) (src dst : Fin n) (c : R) : Hex.Matrix R n m
Hex.Matrix.rowAdd.{u_1} {R : Type u_1}
  {n m : ℕ} [Mul R] [Add R]
  (M : Hex.Matrix R n m) (src dst : Fin n)
  (c : R) : Hex.Matrix R n m

Replace row dst by row dst + c * row src.

The source row is read once into rsrc, so the only remaining reference to M is the consuming Vector.modify, which updates the outer vector in place when M is uniquely referenced (dropping the old row dst). The replacement row is built fresh, since every entry of it changes.