eval₂_X

Mathlib.RingTheory.MvPowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.eval₂_X

English

For the indeterminate X_s, evaluation picks out the corresponding value a_s.

Русский

Для индeterminate X_s оценивание даёт значение a_s.

LaTeX

$$$$\operatorname{eval}_{\phi}^{a}(X_{s}) = a_{s}$$$$

Lean4

@[simp]
theorem eval₂_X (s : σ) : eval₂ φ a (X s) = a s := by rw [← coe_X, eval₂_coe, MvPolynomial.eval₂_X]

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

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

Разделы

Аффилиация

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