erase_sub — Mathlib

English

Erasing commutes with subtraction: erase a (f1 - f2) = erase a f1 - erase a f2.

Русский

Иcключение элемента на позиции a коммутирует с вычитанием: erase a (f1 - f2) = erase a f1 - erase a f2.

LaTeX

$$$\mathrm{erase}(a, f_1 - f_2) = \mathrm{erase}(a, f_1) - \mathrm{erase}(a, f_2)$$$

Lean4

@[simp]
theorem erase_sub (a : ι) (f₁ f₂ : ι →₀ G) : erase a (f₁ - f₂) = erase a f₁ - erase a f₂ :=
  (eraseAddHom a : (_ →₀ G) →+ _).map_sub f₁ f₂

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