vars_sub_subset

Mathlib.Algebra.MvPolynomial.CommRing

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

English

The set of variables appearing in −p is the same as those appearing in p.

Русский

Множество переменных, встречающихся в −p, такое же как в p.

LaTeX

$$$(-p).\\mathrm{vars} = p.\\mathrm{vars}$$$

Lean4

theorem vars_sub_subset [DecidableEq σ] : (p - q).vars ⊆ p.vars ∪ q.vars := by
  convert vars_add_subset p (-q) using 2 <;> simp [sub_eq_add_neg]

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

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

Разделы

Аффилиация

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