coe_of_mul_apply_add — Mathlib

English

The nth component of the product equals the sum of products across all index pairs consistent with i + j = n.

Русский

Компонента на позиции n равна сумме произведений по всем парам индексов, удовлетворяющим i + j = n.

LaTeX

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

Lean4

theorem coe_of_mul_apply_add [AddLeftCancelMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : A i) (r' : ⨁ i, A i)
    (j : ι) : ((of (fun i => A i) i r * r') (i + j) : R) = r * r' j :=
  coe_of_mul_apply_aux _ _ _ fun _x => ⟨fun h => add_left_cancel h, fun h => h ▸ rfl⟩

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