Pso — Mathlib

English

If i^2 = -1, then Pso(p,q,R,i) is invertible with inverse Pso(p,q,R,-i).

Русский

Если i^2 = -1, то Pso(p,q,R,i) имеет обратную Pso(p,q,R,-i).

LaTeX

$$$$ Pso(p,q,R,i) \cdot Pso(p,q,R,-i) = I. $$$$

Lean4

/-- A matrix for transforming the indefinite diagonal bilinear form into the definite one, provided
the parameter `i` is a square root of -1. -/
def Pso (i : R) : Matrix (p ⊕ q) (p ⊕ q) R :=
  Matrix.diagonal <| Sum.elim (fun _ => 1) fun _ => i

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