English
Unit vector: the 1-dimensional holor with 1 in position j and zeros elsewhere.
Русский
Единичный вектор: 1-мерный холор с единицей на позиции j и нулями иначе.
LaTeX
$$$\mathrm{unitVec}\,(d)\,(j) : \ Holor\, \alpha\,[d] = \lambda t. \mathbf{1}_{t=(j)}$$$
Lean4
/-- The 1-dimensional "unit" holor with 1 in the `j`th position. -/
def unitVec [Monoid α] [AddMonoid α] (d : ℕ) (j : ℕ) : Holor α [d] := fun ti => if ti.1 = [j] then 1 else 0