ext_iff — Mathlib

English

Two elements of GL_n(R) are equal iff their matrices agree entrywise.

Русский

Два элемента GL_n(R) равны тогда и только тогда, когда их матрицы совпадают по всем коэффициентам.

LaTeX

$$ext_iff (A B : GL n R) : A = B ↔ ∀ i j, (A : Matrix n n R) i j = (B : Matrix n n R) i j$$

Lean4

theorem ext_iff (A B : GL n R) : A = B ↔ ∀ i j, (A : Matrix n n R) i j = (B : Matrix n n R) i j :=
  Units.ext_iff.trans Matrix.ext_iff.symm

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