`BookProof.Complexification.Cx.cxConj_inner` (x y : Cx W) : inner ℂ (cxConj x) (cxConj y) = starRingEnd ℂ (inner ℂ x y)

Initializing...

`BookProof.Complexification.Cx.cxConj_inner` (x y : Cx W) : inner ℂ (cxConj x) (cxConj y) = starRingEnd ℂ (inner ℂ x y) · Prove2Me