C_mul'

Mathlib.Algebra.Polynomial.Coeff

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

English

Constant multiplication by a in a polynomial equals the scalar multiplication by a: C a · f = a • f.

Русский

Умножение константой на полином равно скалярному умножению на константу: C a · f = a • f.

LaTeX

$$$C a \cdot f = a \cdot f$$$

Lean4

theorem C_mul' (a : R) (f : R[X]) : C a * f = a • f := by
  ext
  rw [coeff_C_mul, coeff_smul, smul_eq_mul]

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

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

Разделы

Аффилиация

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