ext — Mathlib

English

If two elements of GL_n(R) have the same entries, they are equal.

Русский

Если две элементы GL_n(R) имеют одинаковые элементы, они равны.

LaTeX

$$ext ⦃A B : GL n R⦄ (h : ∀ i j, (A : Matrix n n R) i j = (B : Matrix n n R)) : A = B$$

Lean4

/-- Not marked `@[ext]` as the `ext` tactic already solves this. -/
theorem ext ⦃A B : GL n R⦄ (h : ∀ i j, (A : Matrix n n R) i j = (B : Matrix n n R) i j) : A = B :=
  Units.ext <| Matrix.ext h

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