`BookProof.ChapterH5.pow_apply_mem_krylovSpan` {i m : ℕ} (hi : i < m) : (H ^ i) v ∈ krylovSpan H v m
ProvedBookProof.ChapterH5.pow_apply_mem_krylovSpantheoremstimepiece
Prove the following Lean 4 theorem from ChapterH5.
BookProof.ChapterH5.pow_apply_mem_krylovSpan {i m : ℕ} (hi : i < m) : (H ^ i) v ∈ krylovSpan H v m
Formalization note: Lean 4 identifier BookProof.ChapterH5.pow_apply_mem_krylovSpan.
Preamble
-- Generated from ChapterH5.lean — theorem BookProof.ChapterH5.pow_apply_mem_krylovSpan
import Mathlib
import Definitions.Def_ChapterH5
open BookProof.ChapterH5
noncomputable section
variable {K E : Type*} [Field K] [AddCommGroup E] [Module K E]
variable {H : E →ₗ[K] E} {v : E}Formal statement
theorem BookProof.ChapterH5.pow_apply_mem_krylovSpan {i m : ℕ} (hi : i < m) :
(H ^ i) v ∈ krylovSpan H v m := by sorry