smeval_X

Mathlib.Algebra.Polynomial.Smeval

URI: https://scilib.ai/kg/mathlib#Polynomial.smeval_X

English

The smeval of the indeterminate X is x raised to the first power: smeval X x = x^1.

Русский

С smeval переменной X имеем X.smeval x = x^1.

LaTeX

$$$$ X.smeval x = x^1. $$$$

Lean4

@[simp]
theorem smeval_X : (X : R[X]).smeval x = x ^ 1 := by
  simp only [smeval_eq_sum, smul_pow, zero_smul, sum_X_index, one_smul]

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

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

Разделы

Аффилиация

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