expand_X

Mathlib.Algebra.MvPolynomial.Expand

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

English

Expanding the variable X_i by p yields X_i^p.

Русский

Расширение переменной X_i на p даёт X_i^p.

LaTeX

$$$$ \operatorname{expand}(p)(\mathrm{X}_i) = \mathrm{X}_i^p. $$$$

Lean4

@[simp]
theorem expand_X (p : ℕ) (i : σ) : expand p (X i : MvPolynomial σ R) = X i ^ p :=
  eval₂Hom_X' _ _ _

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

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

Разделы

Аффилиация

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