vars_def

Mathlib.Algebra.MvPolynomial.Variables

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

English

Under decidable equality on σ, the same equality holds: vars(p) = degrees(p) toFinset.

Русский

При решаемом равенстве σ то же равенство: vars(p) = degrees(p) toFinset.

LaTeX

$$$$ \mathrm{vars}(p) = (\mathrm{degrees}(p))^{\mathrm{toFinset}} $$$$

Lean4

theorem vars_def [DecidableEq σ] (p : MvPolynomial σ R) : p.vars = p.degrees.toFinset :=
  by
  rw [vars]
  convert rfl

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

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

Разделы

Аффилиация

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