smeval_eq_sum

Mathlib.Algebra.Polynomial.Smeval

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

English

smeval equals the sum expression with smul_pow components.

Русский

smeval равен сумме выражения, включающего компоненты smul_pow.

LaTeX

$$$p.smeval x = p.sum (smul_pow x)$$$

Lean4

theorem smeval_eq_sum : p.smeval x = p.sum (smul_pow x) := by rw [smeval_def]

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

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

Разделы

Аффилиация

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