aeval_monomial

Mathlib.Algebra.Polynomial.AlgebraMap

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

English

aeval x monomial(n,r) equals algebraMap r times x^n.

Русский

aeval x мономиалы(n,r) равен algebraMap r умножить на x^n.

LaTeX

$$$$\mathrm{aeval}_x(\mathrm{monomial}(n, r)) = \mathrm{algebraMap}\ R A\ r \cdot x^{n}.$$$$

Lean4

@[simp]
theorem aeval_monomial {n : ℕ} {r : R} : aeval x (monomial n r) = algebraMap _ _ r * x ^ n :=
  eval₂_monomial _ _

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

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

Разделы

Аффилиация

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