`BookProof.ChapterH3.sirk_krylov_mem_adjoin` (Xm : Module.End ℂ E) (Y X : ℕ → Module.End ℂ E) (hX : ∀ j, X j = Y j * Xm) (v : E) (j : ℕ) : ∃ r ∈ Algebra.adjoin ℂ ({Xm} ∪ Set.range

Initializing...

`BookProof.ChapterH3.sirk_krylov_mem_adjoin` (Xm : Module.End ℂ E) (Y X : ℕ → Module.End ℂ E) (hX : ∀ j, X j = Y j * Xm) (v : E) (j : ℕ) : ∃ r ∈ Algebra.adjoin ℂ ({Xm} ∪ Set.range · Prove2Me