coe_mul_of_apply_of_not_le — Mathlib

English

If i is not less or equal to n, the coefficient at n vanishes when multiplying by a zero-degree component.

Русский

Если i не удовлетворяет i ≤ n, коэффициент при n обращается в ноль при умножении на компонент нулевой степени.

LaTeX

$$$$ (r * of(A) i r')_n = 0 \quad\text{если } i \nle n.$$$$

Lean4

theorem coe_mul_of_apply_of_not_le (r : ⨁ i, A i) {i : ι} (r' : A i) (n : ι) (h : ¬i ≤ n) :
    ((r * of (fun i => A i) i r') n : R) = 0 := by
  classical
  rw [coe_mul_apply_eq_dfinsuppSum, DFinsupp.sum_comm]
  apply (DFinsupp.sum_single_index _).trans
  swap
  · simp_rw [ZeroMemClass.coe_zero, mul_zero, 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_left i x).trans_eq H)

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