reflect_C_mul — Mathlib

English

Reflect distributes over multiplication by constants: reflect N (C r · f) = C r · reflect N f.

Русский

Reflect распространяется на умножение константами: reflect N (C r · f) = C r · reflect N f.

LaTeX

$$$\\mathrm{reflect}\\ N\\ (C\\ r\\cdot f)=C\\ r\\cdot \\mathrm{reflect}\\ N\\ f.$$$

Lean4

@[simp]
theorem reflect_C_mul (f : R[X]) (r : R) (N : ℕ) : reflect N (C r * f) = C r * reflect N f :=
  by
  ext
  simp only [coeff_reflect, coeff_C_mul]

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