coe_of_mul_apply_of_not_le — Mathlib

English

There is a uniform notation for the product of direct sum elements using dfinsupp or sum notation.

Русский

Существует единая нотация произведения элементов прямого суммирования через dfinsupp или сумму.

LaTeX

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

Lean4

theorem coe_of_mul_apply_of_not_le {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι) (h : ¬i ≤ n) :
    ((of (fun i => A i) i r * r') n : R) = 0 := by
  classical
  rw [coe_mul_apply_eq_dfinsuppSum]
  apply (DFinsupp.sum_single_index _).trans
  swap
  · simp_rw [ZeroMemClass.coe_zero, zero_mul, ite_self]
    exact DFinsupp.sum_zero
  · rw [DFinsupp.sum, Finset.sum_ite_of_false, Finset.sum_const_zero]
    exact fun x _ H => h ((self_le_add_right i x).trans_eq H)

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