natCast_mul_comp

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

Composition commutes with multiplication by a natural cast: ((n) * p) ∘ r = n * (p ∘ r).

Русский

Композиция сохраняет умножение на натуральную вставку: ((n) * p) ∘ r = n * (p ∘ r).

LaTeX

$$((n : R[X]) * p) \\circ r = n * (p \\circ r)$$

Lean4

@[simp]
theorem natCast_mul_comp {n : ℕ} : ((n : R[X]) * p).comp r = n * p.comp r := by rw [← C_eq_natCast, C_mul_comp]

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

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

Разделы

Аффилиация

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