qsmul_eq_C_mul

Mathlib.Algebra.Polynomial.Basic

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

← MathLib Explorer

English

For a DivisionRing R, and a polynomial f, a rational a satisfies a • f = C(a) · f for a ∈ ℚ.

Русский

Для полей над R и рационального a выполняется a • f = C(a) · f.

LaTeX

$$a • f = C(a) · f$$

Lean4

theorem qsmul_eq_C_mul (a : ℚ) (f : R[X]) : a • f = Polynomial.C (a : R) * f := by
  rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

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

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

Разделы

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

Аффилиация

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