DMatrix.ext

theorem DMatrix.ext : ∀ {m : Type u_2} {n : Type u_3} {α : m → n → Type v} {M N : DMatrix m n α}, (∀ (i : m) (j : n), M i j = N i j) → M = N

This theorem, `DMatrix.ext`, states that for any two dependently typed matrices `M` and `N` of the same type (`DMatrix m n α`), if for every row index `i` from type `m` and column index `j` from type `n` it holds that the entries at position `(i, j)` in both matrices are identical (i.e., `M i j = N i j`), then the matrices `M` and `N` are equal. In other words, two dependently typed matrices are equal if all their corresponding entries are equal.

More concisely: If for all i and j, the entries M(i, j) and N(i, j) of dependently typed matrices M : DMatrix m n α and N : DMatrix m n α are equal, then matrices M and N are equal.