English
Let i ∈ R with i^2 = -1. Then the conjugation by Pso transforms the indefinite diagonal into the identity: (Pso p q R i)ᵀ · indefiniteDiagonal p q R · Pso p q R i = I.
Русский
Пусть i ∈ R удовлетворяет i^2 = -1. Тогда конъюгация диагональной формы через Pso приводит к тождественной форме: (Pso p q R i)ᵀ · indefiniteDiagonal p q R · Pso p q R i = I.
LaTeX
$$$ (Pso(p,q,R,i))^{\top} \cdot \operatorname{indefiniteDiagonal}(p,q,R) \cdot Pso(p,q,R,i) = I $,$$
Lean4
theorem indefiniteDiagonal_transform {i : R} (hi : i * i = -1) :
(Pso p q R i)ᵀ * indefiniteDiagonal p q R * Pso p q R i = 1 :=
by
ext (x y); rcases x with ⟨x⟩ | ⟨x⟩ <;> rcases y with ⟨y⟩ | ⟨y⟩
· -- x y : p
by_cases h : x = y <;> simp [Pso, indefiniteDiagonal, h, one_apply]
· -- x : p, y : q
simp [Pso, indefiniteDiagonal]
· -- x : q, y : p
simp [Pso, indefiniteDiagonal]
· -- x y : q
by_cases h : x = y <;> simp [Pso, indefiniteDiagonal, h, hi, one_apply]
