English
The isomorphism soIndefiniteEquiv acts on elements A ∈ so′(p,q;R) by conjugation with Pso: soIndefiniteEquiv(p,q,R,i)(A) = Pso(p,q,R,i)^{-1} A Pso(p,q,R,i).
Русский
Применение эквивалента soIndefiniteEquiv к A ∈ so′(p,q;R) есть конъюгация по Pso: soIndefiniteEquiv(p,q,R,i)(A) = Pso(p,q,R,i)^{-1} A Pso(p,q,R,i).
LaTeX
$$$ (soIndefiniteEquiv(p,q,R,i)\,A) = (Pso(p,q,R,i))^{-1} \cdot A \cdot Pso(p,q,R,i). $$$$
Lean4
theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) :
(soIndefiniteEquiv p q R hi A : Matrix (p ⊕ q) (p ⊕ q) R) =
(Pso p q R i)⁻¹ * (A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i :=
by
rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [skewAdjointMatricesLieSubalgebraEquiv_apply]
