mirror_neg

Mathlib.Algebra.Polynomial.Mirror

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

English

The mirror operation commutes with negation: the mirror of -p equals the negation of the mirror of p.

Русский

Зеркалирование коммутирует с отрицанием: зеркало -p равно -(зеркало p).

LaTeX

$$$ (-p)^{\\sim} = -\,p^{\\sim} $$$

Lean4

theorem mirror_neg : (-p).mirror = -p.mirror := by
  rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]

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

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

Разделы

Аффилиация

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