Prove2Me

krylov_li_of_le

Proved
BookProof.ChapterH8.krylov_li_of_le

by leonardopedro · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

formalizationtimepiece

Formal statement of BookProof.ChapterH8.krylov_li_of_le from the timepiece Lean 4 formalization (source chapter BookProof/ChapterH8Bases.lean).

Preamble
-- Generated from ChapterH8Bases.lean — theorem BookProof.ChapterH8.krylov_li_of_le
import Definitions.Def_ChapterH4
import Definitions.Def_ChapterH5
import Definitions.Def_ChapterH6
import Mathlib
import Definitions.Def_ChapterH8Bases
import Definitions.Def_ChapterH8
open BookProof.ChapterH8

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E]


noncomputable section


open BookProof.ChapterH4 BookProof.ChapterH5 BookProof.ChapterH6




open ContinuousLinearMap
Formal statement
theorem BookProof.ChapterH8.krylov_li_of_le {H : E →ₗ[ℂ] E} {v : E} {m n : ℕ} (hmn : m ≤ n)
    (hli : LinearIndependent ℂ (fun i : Fin n => (H ^ (i : ℕ)) v)) :
    LinearIndependent ℂ (fun i : Fin m => (H ^ (i : ℕ)) v) := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterH8Bases.lean

View graph