neg_cancelLeads

Mathlib.Algebra.Polynomial.CancelLeads

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

English

The operation cancelLeads is antisymmetric with respect to negation: -p.cancelLeads q = q.cancelLeads p.

Русский

Операция cancelLeads антисимметрична относительно отрицания: -p.cancelLeads q = q.cancelLeads p.

LaTeX

$$-p.cancelLeads q = q.cancelLeads p$$

Lean4

@[simp]
theorem neg_cancelLeads : -p.cancelLeads q = q.cancelLeads p :=
  neg_sub _ _

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

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

Разделы

Аффилиация

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