ext_iff — Mathlib

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]⟩

Похожие утверждения