(V : F →L[ℂ] E) (X qX qXinv : E →L[ℂ] E) (qBinv : F →L[ℂ] F) (p : Polynomial ℂ) (hVV : (adjoint V).comp V = ContinuousLinearMap.id ℂ F) (hinvX : ∀ x : F, ∃ y : F, X (V x) = V y) (hinvq : ∀ x : F,...

Initializing...

(V : F →L[ℂ] E) (X qX qXinv : E →L[ℂ] E) (qBinv : F →L[ℂ] F) (p : Polynomial ℂ) (hVV : (adjoint V).comp V = ContinuousLinearMap.id ℂ F) (hinvX : ∀ x : F, ∃ y : F, X (V x) = V y) (hinvq : ∀ x : F,... · Prove2Me