smul_comp

Mathlib.Algebra.Polynomial.Eval.SMul

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

← MathLib Explorer

English

(s • p).comp q = s • (p.comp q).

Русский

(s • p).comp q = s • (p.comp q).

LaTeX

$$$ (s \\cdot p).\\operatorname{comp} q = s \\cdot (p.\\operatorname{comp} q) $$$

Lean4

@[simp]
theorem smul_comp [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p q : R[X]) : (s • p).comp q = s • p.comp q := by
  rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]

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

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

Разделы

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

Аффилиация

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