toAddMonoidAlgebra_sub — Mathlib

English

Let f and g be elements of the direct sum ⨁_{ι} M. Then the AddMonoidAlgebra of their difference equals the difference of their AddMonoidAlgebras.

Русский

Пусть f и g — элементы прямой суммы ⨁_{ι} M. Тогда AddMonoidAlgebra от их разности равен разности соответствующих AddMonoidAlgebra.

LaTeX

$$$ (f - g).toAddMonoidAlgebra = toAddMonoidAlgebra\, f - toAddMonoidAlgebra\, g $$$

Lean4

@[simp]
theorem toAddMonoidAlgebra_sub [Ring M] [∀ m : M, Decidable (m ≠ 0)] (f g : ⨁ _ : ι, M) :
    (f - g).toAddMonoidAlgebra = toAddMonoidAlgebra f - toAddMonoidAlgebra g :=
  DFinsupp.toFinsupp_sub _ _

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