toAddMonoidAlgebra_neg — Mathlib

English

Let f be an element of the direct sum ⨁_{ι} M. The AddMonoidAlgebra of its negation equals the negation of its AddMonoidAlgebra.

Русский

Пусть f — элемент прямой суммы. AddMonoidAlgebra от его отрицания равно отрицанию AddMonoidAlgebra f.

LaTeX

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

Lean4

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

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