map_C

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

The map of a constant polynomial is the corresponding constant with the coefficient transformed by f: (C a).map f = C(f a).

Русский

Отображение константного полинома даёт константу с преобразованной коэффициентной частью: (C a).map f = C(f a).

LaTeX

$$$$(C a).map f = C (f a)$$$$

Lean4

@[simp]
theorem map_C : (C a).map f = C (f a) :=
  eval₂_C _ _

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

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

Разделы

Аффилиация

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