vars_neg

Mathlib.Algebra.MvPolynomial.CommRing

URI: https://scilib.ai/kg/mathlib#MvPolynomial.vars_neg

English

The degree of −p with respect to any x is the same as the degree of p with respect to x.

Русский

Степень −p по x равна степени p по x.

LaTeX

$$$\\mathrm{degreeOf}\,i(-p) = \\mathrm{degreeOf}\,i(p)$$$

Lean4

@[simp]
theorem vars_neg : (-p).vars = p.vars := by simp [vars, degrees_neg]

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

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

Разделы

Аффилиация

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