single_tsub — Mathlib

English

For any index i and elements a,b ∈ α_i, the dfinsupp obtained by subtracting a,b at i with a single nonzero coordinate satisfies: single i (a - b) = single i a - single i b.

Русский

Для любого индекса i и элементов a,b ∈ α_i выполняется: single i (a - b) = single i a - single i b.

LaTeX

$$$\text{single } i (a - b) = \text{single } i a - \text{single } i b$$$

Lean4

@[simp]
theorem single_tsub : single i (a - b) = single i a - single i b :=
  by
  ext j
  obtain rfl | h := eq_or_ne j i
  · rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
  · rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]

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