aeval_C

Mathlib.Algebra.MvPolynomial.Eval

URI: https://scilib.ai/kg/mathlib#MvPolynomial.aeval_C

English

The image of a constant under aeval is the corresponding algebra element: aeval f (C r) = algebraMap_R^S1 r.

Русский

Образ константы C r через aeval — это соответствующий элемент в S1: aeval f (C r) = algebraMap_R_S1 r.

LaTeX

$$$\\\\mathrm{aeval} f (C r) = \\\\mathrm{algebraMap} R S_1 r$$$

Lean4

theorem aeval_C (r : R) : aeval f (C r) = algebraMap R S₁ r :=
  eval₂_C _ _ _

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

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

Разделы

Аффилиация

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