coe_mul_apply_eq_sum_antidiagonal

English

The nth coefficient of the product equals the sum over all pairs (i, j) lying on the antidiagonal i + j = n, of r_i · r'_j.

Русский

Коэффициент при n равен сумме по всем парам (i, j), лежащим на антидиагонали i + j = n, от произведений коэффициентов r_i и r'_j.

LaTeX

$$$$(r * r')_n = \\sum_{(i,j) \\in \\text{antidiagonal}(n)} r_i \\; r'_j.$$$

Lean4

theorem coe_mul_apply_eq_sum_antidiagonal [AddMonoid ι] [HasAntidiagonal ι] [SetLike.GradedMonoid A] (r r' : ⨁ i, A i)
    (n : ι) : (r * r') n = ∑ ij ∈ antidiagonal n, (r ij.1 : R) * r' ij.2 := by
  classical
  rw [coe_mul_apply]
  apply Finset.sum_subset (fun _ ↦ by simp)
  aesop (erase simp not_and) (add simp not_and_or)

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