`BookProof.ShiftedQuadraticMatrix.orthonormal_hermiteTRLp` {O : Matrix (Fin d) (Fin d) ℝ} (hO : Oᵀ * O = 1) (a k : Vd d) : Orthonormal ℂ (hermiteTRLp (d := d) O a k)

Initializing...

`BookProof.ShiftedQuadraticMatrix.orthonormal_hermiteTRLp` {O : Matrix (Fin d) (Fin d) ℝ} (hO : Oᵀ * O = 1) (a k : Vd d) : Orthonormal ℂ (hermiteTRLp (d := d) O a k) · Prove2Me