toDirectSum_neg

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

URI: https://scilib.ai/kg/mathlib#AddMonoidAlgebra.toDirectSum_neg

English

Negation in AddMonoidAlgebra corresponds to negation in the DirectSum representation.

Русский

Употребление отрицания в AddMonoidAlgebra соответствует отрицанию в представлении DirectSum.

LaTeX

$$$( -f ).toDirectSum = - f.toDirectSum$$

Lean4

@[simp]
theorem toDirectSum_neg [Ring M] (f : AddMonoidAlgebra M ι) : (-f).toDirectSum = -f.toDirectSum :=
  Finsupp.toDFinsupp_neg _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru