smul_eq_C_mul — Mathlib

English

For any r ∈ R and f ∈ LaurentPolynomial R, the scalar action of r on f equals multiplication by the constant Laurent polynomial C r: r • f = C r * f.

Русский

Пусть r ∈ R и f ∈LaurentPolynomial(R). Тогда скалярное умножение равно умножению на константный лоурентовый многочлен: r • f = C r · f.

LaTeX

$$$\forall r \in R, \forall f \in R[T;T^{-1}]:\ r \cdot f = C(r) \cdot f$$$

Lean4

theorem smul_eq_C_mul (r : R) (f : R[T;T⁻¹]) : r • f = C r * f := by
  induction f using LaurentPolynomial.induction_on' with
  | add _ _ hp hq => rw [smul_add, mul_add, hp, hq]
  | C_mul_T n s =>
    rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C, Finsupp.smul_single',
      single_eq_C]

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