eval_smul'

Mathlib.Algebra.Polynomial.GroupRingAction

URI: https://scilib.ai/kg/mathlib#Polynomial.eval_smul'

← MathLib Explorer

English

If you evaluate the product prodXSubSMul G R x at x itself, the result is 0.

Русский

При вычислении произведения prodXSubSMul G R x в x получаем 0.

LaTeX

$$$\bigl(prodXSubSMul G R x\bigr).eval x = 0$.$$

Lean4

theorem eval_smul' [MulSemiringAction G S] (g : G) (f : S[X]) (x : S) : f.eval (g • x) = g • (g⁻¹ • f).eval x := by
  rw [← smul_eval_smul, smul_inv_smul]

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

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

Разделы

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

Аффилиация

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