vars_map_of_injective

Mathlib.Algebra.MvPolynomial.Variables

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

English

If f is injective, then (map f p).vars = p.vars.

Русский

Если отображение f инъективно, то множества переменных после отображения совпадают: (map f p).vars = p.vars.

LaTeX

$$$ (map\ f\ p).vars = p.vars $$$

Lean4

theorem vars_map_of_injective (hf : Injective f) : (map f p).vars = p.vars := by
  simp [vars, degrees_map_of_injective _ hf]

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

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

Разделы

Аффилиация

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