aeval_monomial

Mathlib.Algebra.MvPolynomial.Eval

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

← MathLib Explorer

English

aeval is additive over finite sums: aeval_f(∑ φ_i) = ∑ aeval_f(φ_i).

Русский

aeval сохраняет сложение: aeval_f(∑ φ_i) = ∑ aeval_f(φ_i).

LaTeX

$$$$ \mathrm{aeval}_f\left( \sum_{i \in s} \phi_i \right) = \sum_{i \in s} \mathrm{aeval}_f(\phi_i) $$$$

Lean4

theorem aeval_monomial (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
    aeval g (monomial d r) = algebraMap _ _ r * d.prod fun i k => g i ^ k :=
  eval₂Hom_monomial _ _ _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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