weight_sub_single_add — Mathlib

English

If f has a nonzero value at i, then (f − single i 1).weight w plus w(i) equals f.weight w.

Русский

Если f(i) ≠ 0, то (f − δ_i^1).weight w + w(i) = f.weight w.

LaTeX

$$((f - single i 1).weight w) + w i = f.weight w$$

Lean4

theorem weight_sub_single_add {f : σ →₀ ℕ} {i : σ} (hi : f i ≠ 0) : (f - single i 1).weight w + w i = f.weight w :=
  by
  conv_rhs => rw [← sub_add_single_one_cancel hi, weight_apply]
  rw [sum_add_index', sum_single_index, one_smul, weight_apply]
  exacts [zero_smul .., fun _ ↦ zero_smul .., fun _ _ _ ↦ add_smul ..]

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