toLaurent_C_mul_eq — Mathlib

English

The Laurent embedding respects multiplication by constants: toLaurent (Polynomial.C r * f) = C r * toLaurent f.

Русский

Вложение лаурентов сохраняет умножение на константы: toLaurent (C r · f) = C r · toLaurent f.

LaTeX

$$$toLaurent (Polynomial.C\\, r * f) = C\\, r * toLaurent f$$$

Lean4

@[simp]
theorem _root_.Polynomial.toLaurent_C_mul_eq (r : R) (f : R[X]) : toLaurent (Polynomial.C r * f) = C r * toLaurent f :=
  by simp only [map_mul, Polynomial.toLaurent_C]

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