(U Om : E →L[ℂ] E) (hcomm : Om.comp U = U.comp Om) (n : ℕ) (v : E) (hv : Om v = 0) : Om ((U ^ n) v) = 0

Initializing...

(U Om : E →L[ℂ] E) (hcomm : Om.comp U = U.comp Om) (n : ℕ) (v : E) (hv : Om v = 0) : Om ((U ^ n) v) = 0 · Prove2Me