unitVec — Mathlib

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

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