mul_coeff_one — Mathlib

English

The coefficient of degree 1 in the product p q is p0 q1 + p1 q0 (assuming p = p0 + p1 X and q = q0 + q1 X).

Русский

Коэффициент при степени 1 множителя p q равен p0 q1 + p1 q0 (при p = p0 + p1 X, q = q0 + q1 X).

LaTeX

$$$\operatorname{coeff}(p q) 1 = \operatorname{coeff}(p) 0 \cdot \operatorname{coeff}(q) 1 + \operatorname{coeff}(p) 1 \cdot \operatorname{coeff}(q) 0$$$

Lean4

theorem mul_coeff_one (p q : R[X]) : coeff (p * q) 1 = coeff p 0 * coeff q 1 + coeff p 1 * coeff q 0 :=
  by
  rw [coeff_mul, Nat.antidiagonal_eq_map]
  simp [sum_range_succ]

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