eval_lsingle

Mathlib.Algebra.Polynomial.Module.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialModule.eval_lsingle

English

For r ∈ R, i ∈ ℕ, m ∈ M, eval r (lsingle R i m) = r^i • m.

Русский

Для r ∈ R, i ∈ ℕ, m ∈ M, вычисление eval_r на lsingle R i m равно r^i умножить на m.

LaTeX

$$$\\operatorname{eval} r (\\operatorname{lsingle} R i m) = r^{i} \\cdot m$$$

Lean4

@[simp]
theorem eval_lsingle (r : R) (i : ℕ) (m : M) : eval r (lsingle R i m) = r ^ i • m :=
  eval_single r i m

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

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

Разделы

Аффилиация

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