indefiniteDiagonal — Mathlib

English

The indefinite diagonal matrix has p entries equal to 1 and q entries equal to -1 on the diagonal.

Русский

Неопределенная диагональная матрица имеет на диагонали p единиц и q минусов.

LaTeX

$$$$ \operatorname{indefiniteDiagonal}(p,q,R) = \operatorname{diag}(\underbrace{1,\dots,1}_{p}, \underbrace{-1,\dots,-1}_{q}). $$$$

Lean4

/-- The indefinite diagonal matrix with `p` 1s and `q` -1s. -/
def indefiniteDiagonal : Matrix (p ⊕ q) (p ⊕ q) R :=
  Matrix.diagonal <| Sum.elim (fun _ => 1) fun _ => -1

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