sum_support_decompose — Mathlib

English

The sum over indices in the support of decompose ℳ r of the r-coordinate equals r.

Русский

Сумма по индексам из поддержки разложения равна r.

LaTeX

$$$\sum_{i\in \operatorname{supp}(\mathrm{decompose}_{\mathcal{M}}(r))} (\mathrm{decompose}_{\mathcal{M}}(r)_i) = r$$$

Lean4

theorem sum_support_decompose [∀ (i) (x : ℳ i), Decidable (x ≠ 0)] (r : M) :
    (∑ i ∈ (decompose ℳ r).support, (decompose ℳ r i : M)) = r :=
  by
  conv_rhs => rw [← (decompose ℳ).symm_apply_apply r, ← sum_support_of (decompose ℳ r)]
  rw [decompose_symm_sum]
  simp_rw [decompose_symm_of]

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