coe_of_mul_apply_of_le — Mathlib

English

Equivalently to antidiagonal decomposition, the product coefficient is a sum over antidiagonal indices of r_i · r'_j.

Русский

Эквивалентно разложению по антидиагонали: коэффициент произведения равен сумме по антидиагональным парам r_i · r'_j.

LaTeX

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

Lean4

theorem coe_of_mul_apply_of_le {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι) (h : i ≤ n) :
    ((of (fun i => A i) i r * r') n : R) = r * r' (n - i) :=
  coe_of_mul_apply_aux _ _ _ fun x => by rw [eq_tsub_iff_add_eq_of_le h, add_comm]

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