sum_finsupport_smul_eq_finsum — Mathlib

English

If x0 ∈ s, then the sum over i in finsupport x0 of f_i(x0) equals 1.

Русский

Если x0 ∈ s, то сумма по i из finsupport x0 функций f_i(x0) равна 1.

LaTeX

$$$\text{If } x_0 \in s:\quad \sum_{i \in ρ.finsupport x_0} ρ(i)(x_0) = 1$$$

Lean4

theorem sum_finsupport_smul_eq_finsum {M : Type*} [AddCommMonoid M] [Module ℝ M] (φ : ι → X → M) :
    ∑ i ∈ ρ.finsupport x₀, ρ i x₀ • φ i x₀ = ∑ᶠ i, ρ i x₀ • φ i x₀ :=
  by
  apply (finsum_eq_sum_of_support_subset _ _).symm
  have : (fun i ↦ (ρ i) x₀ • φ i x₀) = (fun i ↦ (ρ i) x₀) • (fun i ↦ φ i x₀) :=
    funext fun _ => (Pi.smul_apply' _ _ _).symm
  rw [ρ.coe_finsupport x₀, this, support_smul]
  exact inter_subset_left

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