coe_mul_of_apply_of_mem_zero — Mathlib

English

A specialization where coefficients at index i are multiplied with components from the other side, shifting indices accordingly.

Русский

Специализация, где коэффициенты при индексе i умножаются на компоненты с другой стороны, смещая индексы.

LaTeX

$$$$ ((r * of(A) i r')_n) = r_j * r'_k \text{ when } n = j + k, $$$$

Lean4

theorem coe_mul_of_apply_of_mem_zero [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i, A i) (r' : A 0) (j : ι) :
    ((r * of (fun i => A i) 0 r') j : R) = r j * r' :=
  coe_mul_of_apply_aux _ _ _ fun _x => by rw [add_zero]

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