`BookProof.ChapterA3.bilC_conj` (A M : Matrix (Fin 4) (Fin 4) ℂ) (x : Fin 4 → ℂ) : bilC (Aᵀ * M * A) x = bilC M (fun i => ∑ j, A i j * x j)

Initializing...

`BookProof.ChapterA3.bilC_conj` (A M : Matrix (Fin 4) (Fin 4) ℂ) (x : Fin 4 → ℂ) : bilC (Aᵀ * M * A) x = bilC M (fun i => ∑ j, A i j * x j) · Prove2Me