`BookProof.ChapterConditional.pMarg_eq_diagBHB` (B : Matrix Y X 𝕜) (x : X) : ((Bᴴ * B) x x) = ((pMarg B x : ℝ) : 𝕜)

Initializing...

`BookProof.ChapterConditional.pMarg_eq_diagBHB` (B : Matrix Y X 𝕜) (x : X) : ((Bᴴ * B) x x) = ((pMarg B x : ℝ) : 𝕜) · Prove2Me