(b : HilbertBasis ℕ ℂ F) (m : ℕ) : Module.finrank ℂ (galerkinSpan b m) = m

-- Generated from ChapterSirkRitzMinMax.lean — theorem BookProof.RitzMinMax.finrank_galerkinSpan
import Mathlib
import Definitions.Def_ChapterSirkRitzMinMax
open BookProof.RitzMinMax









noncomputable section


open BookProof.HermiteGalerkin BookProof.ChapterSirkRitzSpectrum
open Filter Topology

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

theorem BookProof.RitzMinMax.finrank_galerkinSpan (b : HilbertBasis ℕ ℂ F) (m : ℕ) :
    Module.finrank ℂ (galerkinSpan b m) = m := by sorry