ext_col — Mathlib

English

Two matrices are equal if all their columns are equal, i.e., A = B whenever A.col j = B.col j for every j.

Русский

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

LaTeX

$$$\forall j,\ A.col j = B.col j \Rightarrow A = B$$$

Lean4

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

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