English
Let α be a semiring. For indices i, j with i < d and a holor x of shape ds, the i-th slice of unitVec(d, j) ⊗ x equals x if i = j and equals 0 otherwise.
Русский
Пусть α задана как полугруппа с умножением (полукольцо). Пусть i, j ∈ ℕ с i < d и x ∈ Holor α ds. Тогда i-ой срез единичного вектора unitVec(d, j) ⊗ x равен x, если i = j, и равен 0 в противном случае.
LaTeX
$$$$ \\operatorname{slice}(\\operatorname{unitVec}(d, j) \\otimes x)\\ i\\ hid = \\begin{cases} x, & i = j \\\\ 0, & i \\neq j \\end{cases} $$$$
Lean4
theorem slice_unitVec_mul [Semiring α] {i : ℕ} {j : ℕ} (hid : i < d) (x : Holor α ds) :
slice (unitVec d j ⊗ x) i hid = if i = j then x else 0 :=
funext fun t : HolorIndex ds =>
if h : i = j then by simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
else by simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]; rfl
