ext_row — Mathlib

English

Two matrices are equal if all their rows are equal, i.e., A = B whenever A.row i = B.row i for every i.

Русский

Две матрицы равны тогда и только тогда, когда равны все их строки: A = B при условии A.row i = B.row i для всех i.

LaTeX

$$$\forall i,\ A.row i = B.row i \Rightarrow A = B$$$

Lean4

/-- Two matrices agree if their rows agree. -/
@[local ext]
theorem ext_row {A B : Matrix m n α} (h : ∀ i, A.row i = B.row i) : A = B :=
  ext fun i j => congr_fun (h i) j

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