coord — Mathlib

English

For each i, coord i is the linear functional sending x to the i-th coordinate of x in basis b.

Русский

Для каждого i линейный функционал coord_i отправляет вектор x на i-ю координату его координат в базисе b.

LaTeX

$$$\\mathrm{coord}\\; i : M \\to R = (\\mathrm{lapply}\\ i) \\circ \\uparrow b.\\mathrm{repr}.$$$

Lean4

/-- `b.coord i` is the linear function giving the `i`-th coordinate of a vector
with respect to the basis `b`.

`b.coord i` is an element of the dual space. In particular, for
finite-dimensional spaces it is the `ι`th basis vector of the dual space.
-/
@[simps!]
def coord : M →ₗ[R] R :=
  Finsupp.lapply i ∘ₗ ↑b.repr

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