apply

Mathlib.LinearAlgebra.Matrix.Symmetric

URI: https://scilib.ai/kg/mathlib#Matrix.IsSymm.apply

English

If A is symmetric, then for all i, j we have A_{j i} = A_{i j}. Equivalently, the same equality holds by applying the symmetry to indices.

Русский

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

LaTeX

$$$\text{IsSymm}(A) \Rightarrow \forall i,j\, A_{j i} = A_{i j}$$$

Lean4

theorem apply {A : Matrix n n α} (h : A.IsSymm) (i j : n) : A j i = A i j :=
  IsSymm.ext_iff.1 h i j

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru