IsDiag

Mathlib.LinearAlgebra.Matrix.IsDiag

URI: https://scilib.ai/kg/mathlib#Matrix.IsDiag

English

A square matrix is diagonal if all off-diagonal entries are zero.

Русский

Квадратная матрица диагональная, если все элементы вне диагонали равны нулю.

LaTeX

$$$A \text{ is diagonal }\Leftrightarrow \forall i \neq j,\ A_{ij}=0.$$$

Lean4

/-- `A.IsDiag` means square matrix `A` is a diagonal matrix. -/
def IsDiag [Zero α] (A : Matrix n n α) : Prop :=
  Pairwise fun i j => A i j = 0

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

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

Разделы

Аффилиация

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