coe_mul_of_apply_add — Mathlib

English

Under appropriate associativity and grading hypotheses, the multiplication of direct sum elements distributes with respect to the grading, giving the same coefficient rule as above.

Русский

При заданных условий ассоциации и градации умножение элементов прямого суммирования распределяется по градам так же, как и выше.

LaTeX

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

Lean4

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

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