units_coeff_zero_smul — Mathlib

English

If c is a unit in the polynomial ring R[X] and p is a polynomial, then the scalar by the constant term of c equals multiplication by c on p, i.e., (coeff 0 c) · p = c · p.

Русский

Пусть c — единица в кольце полиномов R[X], а p — полином. Тогда скалярное умножение на константный коэффициент c равно умножению на сам полином c: (coeff 0 c) · p = c · p.

LaTeX

$$$ (c : R[X]).coeff 0 \cdot p = c \cdot p $$$

Lean4

theorem units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p := by
  rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]

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