jb_transform — Mathlib

English

PB acts by a similarity transformation on JB into a diagonal form involving S: (PB)ᵀ · JB · PB = 2 · S.

Русский

PB осуществляет подобное преобразование JB в диагональную форму с участием S: (PB)ᵀ · JB · PB = 2 · S.

LaTeX

$$$ (PB(l,R))^{\top} \cdot JB(l,R) \cdot PB(l,R) = 2 \cdot S(l,R). $$$

Lean4

theorem jb_transform : (PB l R)ᵀ * JB l R * PB l R = (2 : R) • Matrix.fromBlocks 1 0 0 (S l R) := by
  simp [PB, JB, jd_transform, Matrix.fromBlocks_transpose, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]

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