ext — Mathlib

English

If A is symmetric, then ∀ i, j, A_{j i} = A_{i j}. Conversely, if ∀ i, j A_{j i} = A_{i j}, then A is symmetric.

Русский

Если A симметрична, то ∀ i, j выполняется A_{j i} = A_{i j}. И наоборот, если ∀ i, j выполняется A_{j i} = A_{i j}, то A симметрична.

LaTeX

$$$ A^{\top} = A \iff \forall i,j\, A_{j i} = A_{i j} $$$

Lean4

/-- A version of `Matrix.ext` that unfolds the `Matrix.transpose`. -/
theorem ext {A : Matrix n n α} : (∀ i j, A j i = A i j) → A.IsSymm :=
  Matrix.ext

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