pd_inv — Mathlib

English

PD(l,R) is invertible after multiplying by (1/2) and transposing PD, yielding the identity.

Русский

PD(l,R) инвертируемая после умножения на (1/2) и транспонирования PD, давая тождество.

LaTeX

$$$ PD(l,R) \cdot \left( \tfrac{1}{2} \ PD(l,R)^{\top} \right) = I. $$$

Lean4

theorem pd_inv [Fintype l] [Invertible (2 : R)] : PD l R * ⅟(2 : R) • (PD l R)ᵀ = 1 :=
  by
  rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul, Matrix.fromBlocks_multiply]
  simp

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