single_sub — Mathlib

English

The single term is additive with subtraction: single a (r - s) = single a r - single a s.

Русский

Единичный член сохраняет сложение при вычитании: single a (r - s) = single a r - single a s.

LaTeX

$$$$ \operatorname{single} a (r - s) = \operatorname{single} a r - \operatorname{single} a s. $$$$

Lean4

@[simp]
theorem single_sub (a : Γ) (r s : R) : single a (r - s) = single a r - single a s :=
  map_sub (single.addMonoidHom a) _ _

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