sum_eq_zero_of_mem_span_completeFamily

English

The family completeFamily is linearly independent over ℝ.

Русский

Семейство completeFamily линейно независимо над ℝ.

LaTeX

$$$\text{LinearIndependent}_{\mathbb{R}}(\text{completeFamily})$$$

Lean4

theorem sum_eq_zero_of_mem_span_completeFamily {x : realSpace K}
    (hx : x ∈ Submodule.span ℝ (Set.range fun w : { w // w ≠ w₀ } ↦ completeFamily K w.1)) : ∑ w, x w = 0 := by
  induction hx using Submodule.span_induction with
  | mem _ h =>
    obtain ⟨w, rfl⟩ := h
    simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _), Units.norm, Rat.cast_one,
      Real.log_one]
  | zero => simp
  | add _ _ _ _ hx hy => simp [sum_add_distrib, hx, hy]
  | smul _ _ _ hx => simp [← mul_sum, hx]

Похожие утверждения