`BookProof.ShiftedQuadraticMatrix.rotConj_det` {O : Matrix (Fin d) (Fin d) ℝ} (hO : Oᵀ * O = 1) (c : Fin d → ℝ) : (rotConj O c).det = ∏ i, c i

Initializing...

`BookProof.ShiftedQuadraticMatrix.rotConj_det` {O : Matrix (Fin d) (Fin d) ℝ} (hO : Oᵀ * O = 1) (c : Fin d → ℝ) : (rotConj O c).det = ∏ i, c i · Prove2Me