English
There is an algebra structure on the subtype of R consisting of elements lying in A(0).
Русский
Существует структура Algebra на подтипе R, состоящем из элементов, принадлежащих A(0).
LaTeX
$$Algebra (Subtype \{ x : R | x ∈ A_0 \}) R$$
Lean4
theorem mul_apply_eq_zero {r r' : ⨁ i, A i} {m n : ι} (hr : ∀ i < m, r i = 0) (hr' : ∀ i < n, r' i = 0) ⦃k : ι⦄
(hk : k < m + n) : (r * r') k = 0 := by
classical
rw [Subtype.ext_iff, ZeroMemClass.coe_zero, coe_mul_apply]
apply Finset.sum_eq_zero fun x hx ↦ ?_
obtain (hx | hx) : x.1 < m ∨ x.2 < n := by
by_contra! h
obtain ⟨hm, hn⟩ := h
obtain rfl : x.1 + x.2 = k := by simp_all
apply lt_irrefl (m + n) <| lt_of_le_of_lt (by gcongr) hk
all_goals simp [hr, hr', hx]
