English
The first coefficient of the product φ ψ expresses as a bilinear form in the first coefficients and constants.
Русский
Первый коэффициент произведения φ ψ выражается как линейно-биективная комбинация первых коэффициентов и констант.
LaTeX
$$$\operatorname{coeff}_1(\phi \cdot \psi) = \operatorname{coeff}_1\phi \cdot \operatorname{constantCoeff}\psi + \operatorname{coeff}_1\psi \cdot \operatorname{constantCoeff}\phi$$$
Lean4
/-- First coefficient of the product of two power series. -/
theorem coeff_one_mul (φ ψ : R⟦X⟧) : coeff 1 (φ * ψ) = coeff 1 φ * constantCoeff ψ + coeff 1 ψ * constantCoeff φ :=
by
have : Finset.antidiagonal 1 = {(0, 1), (1, 0)} := by exact rfl
rw [coeff_mul, this, Finset.sum_insert, Finset.sum_singleton, coeff_zero_eq_constantCoeff, mul_comm, add_comm]
simp
