English
The j-th component of the i-th slot equals x if i = j and 0 otherwise.
Русский
j-й компонент слота i равен x, если i = j, и нулю в противном случае.
LaTeX
$$$$\\bigl(\\text{of}(\\lambda i\\mapsto \\{ x\\; \\text{in} \\; A_i\\})\\; i\\; x\\bigr)\\; j = \\begin{cases} x, & j=i, \\\\ 0, & j\\neq i. \\end{cases}$$$$
Lean4
theorem coe_of_apply {M S : Type*} [DecidableEq ι] [AddCommMonoid M] [SetLike S M] [AddSubmonoidClass S M] {A : ι → S}
(i j : ι) (x : A i) : (of (fun i ↦ { x // x ∈ A i }) i x j : M) = if i = j then x else 0 :=
by
obtain rfl | h := Decidable.eq_or_ne j i
· rw [DirectSum.of_eq_same, if_pos rfl]
· rw [DirectSum.of_eq_of_ne _ _ _ h, if_neg h.symm, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]
