`BookProof.ChapterH8.adjoint_aeval` (A : F →L[ℂ] F) (p : Polynomial ℂ) : adjoint (Polynomial.aeval A p) = Polynomial.aeval (adjoint A) (p.map (starRingEnd ℂ))

Initializing...

`BookProof.ChapterH8.adjoint_aeval` (A : F →L[ℂ] F) (p : Polynomial ℂ) : adjoint (Polynomial.aeval A p) = Polynomial.aeval (adjoint A) (p.map (starRingEnd ℂ)) · Prove2Me