English
Let M and N be matrices in CStarMatrix m n A. Then M and N are equal if and only if all corresponding entries coincide: M_{i j} = N_{i j} for every i and j.
Русский
Пусть M и N — матрицы в CStarMatrix m n A. Тогда M = N тогда и только тогда, когда соответствующие элементы совпадают: M_{i j} = N_{i j} для всех i, j.
LaTeX
$$$\\forall {M,N : CStarMatrix m n A}, (\\forall i j, M i j = N i j) \\iff M = N$$$
Lean4
theorem ext_iff {M N : CStarMatrix m n A} : (∀ i j, M i j = N i j) ↔ M = N :=
⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩