smeval_monomial

Mathlib.Algebra.Polynomial.Smeval

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

← MathLib Explorer

English

The smeval of a monomial (monomial n r) is r times x^n under the action.

Русский

smeval для монома (monomial n r) равен r × x^n.

LaTeX

$$$\text{(monomial } n r).smeval x = r \cdot x^n$$$

Lean4

@[simp]
theorem smeval_monomial (n : ℕ) : (monomial n r).smeval x = r • x ^ n := by
  simp only [smeval_eq_sum, smul_pow, zero_smul, sum_monomial_index]

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

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

Разделы

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

Аффилиация

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