rename_X

Mathlib.Algebra.MvPolynomial.Rename

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

English

For each i ∈ σ, the renamed variable is X_{f(i)}: rename_f(X_i) = X_{f(i)}.

Русский

Пусть i ∈ σ, тогда переименованная переменная равна X_{f(i)}: rename_f(X_i) = X_{f(i)}.

LaTeX

$$$\\text{rename}_f(X_i) = X_{f(i)}.$$$

Lean4

@[simp]
theorem rename_X (f : σ → τ) (i : σ) : rename f (X i : MvPolynomial σ R) = X (f i) :=
  eval₂_X _ _ _

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

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

Разделы

Аффилиация

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