toFinsupp_neg

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.toFinsupp_neg

English

For any polynomial a over a ring, the finsupp embedding preserves negation: (−a).toFinsupp = −a.toFinsupp.

Русский

Для любого полинома над кольцом отображение toFinsupp сохраняет отрицание: (−a).toFinsupp = −a.toFinsupp.

LaTeX

$$$(-a)^{\\wedge} = -a^{\\wedge}$$$

Lean4

@[simp]
theorem toFinsupp_neg {R : Type u} [Ring R] (a : R[X]) : (-a).toFinsupp = -a.toFinsupp := by rw [← ofFinsupp_neg]

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

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

Разделы

Аффилиация

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