def Hex.Matrix.pad {R : Type u} {n m : Nat} [OfNat R 0] (M : Matrix R n m) (n' m' : Nat) : Matrix R n' m'

M embedded in the top-left corner of an n' × m' matrix, with zeros filling the rest. Truncation semantics: an entry whose row is ≥ n or column is ≥ m is 0, and if n' < n or m' < m the overhanging entries of M are dropped. The padding lemmas below assume n ≤ n' / m ≤ m', the regime where this is genuine zero-padding.

Equations

• M.pad n' m' = Hex.Matrix.ofFn fun (i : Fin n') (j : Fin m') => if h : ↑i < n ∧ ↑j < m then M[(⟨↑i, ⋯⟩, ⟨↑j, ⋯⟩)] else 0

theorem Hex.Matrix.getElem_pad {R : Type u} {n m : Nat} [OfNat R 0] (M : Matrix R n m) (n' m' : Nat) (i : Fin n') (j : Fin m') : (M.pad n' m')[i][j] = if h : ↑i < n ∧ ↑j < m then M[(⟨↑i, ⋯⟩, ⟨↑j, ⋯⟩)] else 0

Entry formula for a padded matrix: the original entry inside the block, 0 outside.

theorem Hex.Matrix.takeCols_takeRows_pad {R : Type u} {n m : Nat} [OfNat R 0] (M : Matrix R n m) (n' m' : Nat) (hn : n ≤ n') (hm : m ≤ m') : ((M.pad n' m').takeRows n hn).takeCols m hm = M

Taking the top-left n × m block of pad M n' m' returns M.

theorem Hex.Matrix.row_pad {R : Type u} {n m : Nat} [OfNat R 0] (M : Matrix R n m) (n' m' : Nat) (I : Fin n') (hI : ↑I < n) : (M.pad n' m').row I = Vector.ofFn fun (t : Fin m') => if h : ↑t < m then M[(⟨↑I, hI⟩, ⟨↑t, h⟩)] else 0

An in-range row of a padded matrix is the source row followed by zeros.

theorem Hex.Matrix.col_pad {R : Type u} {n m : Nat} [OfNat R 0] (M : Matrix R n m) (n' m' : Nat) (J : Fin m') (hJ : ↑J < m) : (M.pad n' m').col J = Vector.ofFn fun (t : Fin n') => if h : ↑t < n then M[(⟨↑t, h⟩, ⟨↑J, hJ⟩)] else 0

An in-range column of a padded matrix is the source column followed by zeros.

theorem Hex.Matrix.takeCols_takeRows_mul_pad {R : Type u} {n m k : Nat} [Lean.Grind.Ring R] (A : Matrix R n m) (B : Matrix R m k) (n' m' k' : Nat) (hn : n ≤ n') (hm : m ≤ m') (hk : k ≤ k') : (((A.pad n' m').mul (B.pad m' k')).takeRows n hn).takeCols k hk = A.mul B

Padding lemma. Zero-padding each operand to a common larger middle dimension and reading back the top-left n × k block of the product returns the unpadded product A * B. The border entries are zero, so every extended term of each dot product is 0 * _ or _ * 0 and drops out (dotProduct_extendZero).