eval₂_C

Mathlib.RingTheory.PowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#PowerSeries.eval₂_C

English

The evaluation of the indeterminate X at a is a.

Русский

Оценка индетерминанта X равна a.

LaTeX

$$$\text{eval}_2 φ\, a\, X = a$$$

Lean4

@[simp]
theorem eval₂_C (r : R) : eval₂ φ a (C r) = φ r := by rw [← Polynomial.coe_C, eval₂_coe, Polynomial.eval₂_C]

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

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

Разделы

Аффилиация

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