ext_iff — Mathlib

English

Equality of unitary matrices is determined entrywise: two unitary elements are equal iff all their entries coincide.

Русский

Равенство двух унитарных матриц определяется по элементам: равны тогда и только тогда, когда все элементы совпадают.

LaTeX

$$$A = B \\iff \\forall i,j, A_{ij} = B_{ij}$, для $A,B \\in \\mathrm{unitaryGroup}(n,\\alpha)$.$$

Lean4

theorem ext_iff (A B : unitaryGroup n α) : A = B ↔ ∀ i j, A i j = B i j :=
  Subtype.ext_iff.trans ⟨fun h i j => congr_fun (congr_fun h i) j, Matrix.ext⟩

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