mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Bases
/-- There exists a coefficient scaling `e n` to match `(succSub D.P n) x`.  -/
SchauderBasis.RankOneDecomposition.exists_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (D : SchauderBasis.RankOneDecomposition 𝕜 X) (n : ℕ) (x : X),
  ∃ c, c • D.e n = (SchauderBasis.succSub D.P n) x