single_neg

Mathlib.Algebra.SkewMonoidAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#SkewMonoidAlgebra.single_neg

English

The singleton at a with coefficient -b equals the negation of the singleton at a with coefficient b.

Русский

Одиночный элемент на a с коэффициентом -b равен отрицанию одиночного элемента на a с коэффициентом b.

LaTeX

$$$$ single a (-b) = - single a b $$$$

Lean4

@[simp]
theorem single_neg (a : G) (b : k) : single a (-b) = -single a b := by simp [← ofFinsupp_single]

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

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

Разделы

Аффилиация

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